Metamath Proof Explorer

Theorem ifpororb

Description: Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

Ref Expression
Assertion ifpororb ⊢ if- φ ψ ∨ χ θ ∨ τ ↔ if- φ ψ θ ∨ if- φ χ τ

Proof

Step Hyp Ref Expression
1 dfifp2 ⊢ if- φ ψ ∨ χ θ ∨ τ ↔ φ → ψ ∨ χ ∧ ¬ φ → θ ∨ τ
2 df-or ⊢ ψ ∨ χ ↔ ¬ ψ → χ
3 2 imbi2i ⊢ φ → ψ ∨ χ ↔ φ → ¬ ψ → χ
4 df-or ⊢ θ ∨ τ ↔ ¬ θ → τ
5 4 imbi2i ⊢ ¬ φ → θ ∨ τ ↔ ¬ φ → ¬ θ → τ
6 3 5 anbi12i ⊢ φ → ψ ∨ χ ∧ ¬ φ → θ ∨ τ ↔ φ → ¬ ψ → χ ∧ ¬ φ → ¬ θ → τ
7 ifpimimb ⊢ if- φ ¬ ψ → χ ¬ θ → τ ↔ if- φ ¬ ψ ¬ θ → if- φ χ τ
8 dfifp2 ⊢ if- φ ¬ ψ → χ ¬ θ → τ ↔ φ → ¬ ψ → χ ∧ ¬ φ → ¬ θ → τ
9 imor ⊢ if- φ ¬ ψ ¬ θ → if- φ χ τ ↔ ¬ if- φ ¬ ψ ¬ θ ∨ if- φ χ τ
10 ifpnot23d ⊢ ¬ if- φ ¬ ψ ¬ θ ↔ if- φ ψ θ
11 10 orbi1i ⊢ ¬ if- φ ¬ ψ ¬ θ ∨ if- φ χ τ ↔ if- φ ψ θ ∨ if- φ χ τ
12 9 11 bitri ⊢ if- φ ¬ ψ ¬ θ → if- φ χ τ ↔ if- φ ψ θ ∨ if- φ χ τ
13 7 8 12 3bitr3i ⊢ φ → ¬ ψ → χ ∧ ¬ φ → ¬ θ → τ ↔ if- φ ψ θ ∨ if- φ χ τ
14 1 6 13 3bitri ⊢ if- φ ψ ∨ χ θ ∨ τ ↔ if- φ ψ θ ∨ if- φ χ τ