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- ( 𝜏 , 𝜂 , 𝜁 ) ) )

Proof

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- ( 𝜏 , 𝜂 , 𝜁 ) ) )