Theorem: impliesOrImplies4 (NazgandLean4/Prop.lean)

State before:
p₀ p₁ p₂ p₃ r : Prop
⊢ (p₀ → r) ∧ (p₁ → r) ∧ (p₂ → r) ∧ (p₃ → r) ↔ p₀ ∨ p₁ ∨ p₂ ∨ p₃ → r
Tactic:
tauto
State after:
no goals