Metamath Proof Explorer


Theorem ifpbibib

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

Ref Expression
Assertion ifpbibib if- φ ψ χ θ τ if- φ ψ θ if- φ χ τ

Proof

Step Hyp Ref Expression
1 dfifp2 if- φ ψ χ θ τ φ ψ χ ¬ φ θ τ
2 dfbi2 ψ χ ψ χ χ ψ
3 2 imbi2i φ ψ χ φ ψ χ χ ψ
4 jcab φ ψ χ χ ψ φ ψ χ φ χ ψ
5 3 4 bitri φ ψ χ φ ψ χ φ χ ψ
6 dfbi2 θ τ θ τ τ θ
7 6 imbi2i ¬ φ θ τ ¬ φ θ τ τ θ
8 jcab ¬ φ θ τ τ θ ¬ φ θ τ ¬ φ τ θ
9 7 8 bitri ¬ φ θ τ ¬ φ θ τ ¬ φ τ θ
10 5 9 anbi12i φ ψ χ ¬ φ θ τ φ ψ χ φ χ ψ ¬ φ θ τ ¬ φ τ θ
11 an4 φ ψ χ φ χ ψ ¬ φ θ τ ¬ φ τ θ φ ψ χ ¬ φ θ τ φ χ ψ ¬ φ τ θ
12 10 11 bitri φ ψ χ ¬ φ θ τ φ ψ χ ¬ φ θ τ φ χ ψ ¬ φ τ θ
13 dfifp2 if- φ ψ χ θ τ φ ψ χ ¬ φ θ τ
14 ifpimimb if- φ ψ χ θ τ if- φ ψ θ if- φ χ τ
15 13 14 bitr3i φ ψ χ ¬ φ θ τ if- φ ψ θ if- φ χ τ
16 dfifp2 if- φ χ ψ τ θ φ χ ψ ¬ φ τ θ
17 ifpimimb if- φ χ ψ τ θ if- φ χ τ if- φ ψ θ
18 16 17 bitr3i φ χ ψ ¬ φ τ θ if- φ χ τ if- φ ψ θ
19 15 18 anbi12i φ ψ χ ¬ φ θ τ φ χ ψ ¬ φ τ θ if- φ ψ θ if- φ χ τ if- φ χ τ if- φ ψ θ
20 dfbi2 if- φ ψ θ if- φ χ τ if- φ ψ θ if- φ χ τ if- φ χ τ if- φ ψ θ
21 19 20 bitr4i φ ψ χ ¬ φ θ τ φ χ ψ ¬ φ τ θ if- φ ψ θ if- φ χ τ
22 1 12 21 3bitri if- φ ψ χ θ τ if- φ ψ θ if- φ χ τ