Metamath Proof Explorer

Theorem ifpbi123dOLD

Description: Obsolete version of ifpbi123d as of 17-Apr-2024. (Contributed by AV, 30-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ifpbi123d.1 φ ψ τ
ifpbi123d.2 φ χ η
ifpbi123d.3 φ θ ζ
Assertion ifpbi123dOLD φ if- ψ χ θ if- τ η ζ


Step Hyp Ref Expression
1 ifpbi123d.1 φ ψ τ
2 ifpbi123d.2 φ χ η
3 ifpbi123d.3 φ θ ζ
4 1 2 anbi12d φ ψ χ τ η
5 1 notbid φ ¬ ψ ¬ τ
6 5 3 anbi12d φ ¬ ψ θ ¬ τ ζ
7 4 6 orbi12d φ ψ χ ¬ ψ θ τ η ¬ τ ζ
8 df-ifp if- ψ χ θ ψ χ ¬ ψ θ
9 df-ifp if- τ η ζ τ η ¬ τ ζ
10 7 8 9 3bitr4g φ if- ψ χ θ if- τ η ζ