Metamath Proof Explorer

Theorem ifpananb

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

Ref Expression
Assertion ifpananb ⊢ if- φ ψ ∧ χ θ ∧ τ ↔ if- φ ψ θ ∧ if- φ χ τ

Proof

Step Hyp Ref Expression
1 anor ⊢ ψ ∧ χ ↔ ¬ ¬ ψ ∨ ¬ χ
2 anor ⊢ θ ∧ τ ↔ ¬ ¬ θ ∨ ¬ τ
3 ifpbi23 ⊢ ψ ∧ χ ↔ ¬ ¬ ψ ∨ ¬ χ ∧ θ ∧ τ ↔ ¬ ¬ θ ∨ ¬ τ → if- φ ψ ∧ χ θ ∧ τ ↔ if- φ ¬ ¬ ψ ∨ ¬ χ ¬ ¬ θ ∨ ¬ τ
4 1 2 3 mp2an ⊢ if- φ ψ ∧ χ θ ∧ τ ↔ if- φ ¬ ¬ ψ ∨ ¬ χ ¬ ¬ θ ∨ ¬ τ
5 ifpororb ⊢ if- φ ¬ ψ ∨ ¬ χ ¬ θ ∨ ¬ τ ↔ if- φ ¬ ψ ¬ θ ∨ if- φ ¬ χ ¬ τ
6 ifpnotnotb ⊢ if- φ ¬ ψ ¬ θ ↔ ¬ if- φ ψ θ
7 ifpnotnotb ⊢ if- φ ¬ χ ¬ τ ↔ ¬ if- φ χ τ
8 6 7 orbi12i ⊢ if- φ ¬ ψ ¬ θ ∨ if- φ ¬ χ ¬ τ ↔ ¬ if- φ ψ θ ∨ ¬ if- φ χ τ
9 5 8 bitri ⊢ if- φ ¬ ψ ∨ ¬ χ ¬ θ ∨ ¬ τ ↔ ¬ if- φ ψ θ ∨ ¬ if- φ χ τ
10 9 notbii ⊢ ¬ if- φ ¬ ψ ∨ ¬ χ ¬ θ ∨ ¬ τ ↔ ¬ ¬ if- φ ψ θ ∨ ¬ if- φ χ τ
11 ifpnotnotb ⊢ if- φ ¬ ¬ ψ ∨ ¬ χ ¬ ¬ θ ∨ ¬ τ ↔ ¬ if- φ ¬ ψ ∨ ¬ χ ¬ θ ∨ ¬ τ
12 anor ⊢ if- φ ψ θ ∧ if- φ χ τ ↔ ¬ ¬ if- φ ψ θ ∨ ¬ if- φ χ τ
13 10 11 12 3bitr4i ⊢ if- φ ¬ ¬ ψ ∨ ¬ χ ¬ ¬ θ ∨ ¬ τ ↔ if- φ ψ θ ∧ if- φ χ τ
14 4 13 bitri ⊢ if- φ ψ ∧ χ θ ∧ τ ↔ if- φ ψ θ ∧ if- φ χ τ