Metamath Proof Explorer


Theorem ifpbi13

Description: Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 simpl φ ψ χ θ φ ψ
2 1 imbi1d φ ψ χ θ φ τ ψ τ
3 notbi φ ψ ¬ φ ¬ ψ
4 imbi12 ¬ φ ¬ ψ χ θ ¬ φ χ ¬ ψ θ
5 3 4 sylbi φ ψ χ θ ¬ φ χ ¬ ψ θ
6 5 imp φ ψ χ θ ¬ φ χ ¬ ψ θ
7 2 6 anbi12d φ ψ χ θ φ τ ¬ φ χ ψ τ ¬ ψ θ
8 dfifp2 if- φ τ χ φ τ ¬ φ χ
9 dfifp2 if- ψ τ θ ψ τ ¬ ψ θ
10 7 8 9 3bitr4g φ ψ χ θ if- φ τ χ if- ψ τ θ