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- ψ θ η φ ¬ ψ χ θ ψ φ τ θ φ ψ χ η ¬ ψ φ τ η