Metamath Proof Explorer

Theorem ifpor123g

Description: Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020)

Ref Expression
Assertion ifpor123g ⊢ if- φ χ τ ∨ if- ψ θ η ↔ φ → ¬ ψ ∨ χ ∨ θ ∧ ψ → φ ∨ τ ∨ θ ∧ φ → ψ ∨ χ ∨ η ∧ ¬ ψ → φ ∨ τ ∨ η

Proof

Step Hyp Ref Expression
1 df-or ⊢ if- φ χ τ ∨ if- ψ θ η ↔ ¬ if- φ χ τ → if- ψ θ η
2 ifpnot23 ⊢ ¬ if- φ χ τ ↔ if- φ ¬ χ ¬ τ
3 2 imbi1i ⊢ ¬ if- φ χ τ → if- ψ θ η ↔ if- φ ¬ χ ¬ τ → if- ψ θ η
4 1 3 bitri ⊢ if- φ χ τ ∨ if- ψ θ η ↔ if- φ ¬ χ ¬ τ → if- ψ θ η
5 ifpim123g ⊢ if- φ ¬ χ ¬ τ → if- ψ θ η ↔ φ → ¬ ψ ∨ ¬ χ → θ ∧ ψ → φ ∨ ¬ τ → θ ∧ φ → ψ ∨ ¬ χ → η ∧ ¬ ψ → φ ∨ ¬ τ → η
6 4 5 bitri ⊢ if- φ χ τ ∨ if- ψ θ η ↔ φ → ¬ ψ ∨ ¬ χ → θ ∧ ψ → φ ∨ ¬ τ → θ ∧ φ → ψ ∨ ¬ χ → η ∧ ¬ ψ → φ ∨ ¬ τ → η
7 pm4.64 ⊢ ¬ χ → θ ↔ χ ∨ θ
8 7 orbi2i ⊢ φ → ¬ ψ ∨ ¬ χ → θ ↔ φ → ¬ ψ ∨ χ ∨ θ
9 pm4.64 ⊢ ¬ τ → θ ↔ τ ∨ θ
10 9 orbi2i ⊢ ψ → φ ∨ ¬ τ → θ ↔ ψ → φ ∨ τ ∨ θ
11 8 10 anbi12i ⊢ φ → ¬ ψ ∨ ¬ χ → θ ∧ ψ → φ ∨ ¬ τ → θ ↔ φ → ¬ ψ ∨ χ ∨ θ ∧ ψ → φ ∨ τ ∨ θ
12 pm4.64 ⊢ ¬ χ → η ↔ χ ∨ η
13 12 orbi2i ⊢ φ → ψ ∨ ¬ χ → η ↔ φ → ψ ∨ χ ∨ η
14 pm4.64 ⊢ ¬ τ → η ↔ τ ∨ η
15 14 orbi2i ⊢ ¬ ψ → φ ∨ ¬ τ → η ↔ ¬ ψ → φ ∨ τ ∨ η
16 13 15 anbi12i ⊢ φ → ψ ∨ ¬ χ → η ∧ ¬ ψ → φ ∨ ¬ τ → η ↔ φ → ψ ∨ χ ∨ η ∧ ¬ ψ → φ ∨ τ ∨ η
17 11 16 anbi12i ⊢ φ → ¬ ψ ∨ ¬ χ → θ ∧ ψ → φ ∨ ¬ τ → θ ∧ φ → ψ ∨ ¬ χ → η ∧ ¬ ψ → φ ∨ ¬ τ → η ↔ φ → ¬ ψ ∨ χ ∨ θ ∧ ψ → φ ∨ τ ∨ θ ∧ φ → ψ ∨ χ ∨ η ∧ ¬ ψ → φ ∨ τ ∨ η
18 6 17 bitri ⊢ if- φ χ τ ∨ if- ψ θ η ↔ φ → ¬ ψ ∨ χ ∨ θ ∧ ψ → φ ∨ τ ∨ θ ∧ φ → ψ ∨ χ ∨ η ∧ ¬ ψ → φ ∨ τ ∨ η