Theorem ifpbi123d

Description: Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020) (Proof shortened by Wolf Lammen, 17-Apr-2024)

	Ref	Expression
Hypotheses	ifpbi123d.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜏 ) )
	ifpbi123d.2	⊢ ( 𝜑 → ( 𝜒 ↔ 𝜂 ) )
	ifpbi123d.3	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜁 ) )
Assertion	ifpbi123d	⊢ ( 𝜑 → ( if- ( 𝜓 , 𝜒 , 𝜃 ) ↔ if- ( 𝜏 , 𝜂 , 𝜁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ifpbi123d.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜏 ) )
2		ifpbi123d.2	⊢ ( 𝜑 → ( 𝜒 ↔ 𝜂 ) )
3		ifpbi123d.3	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜁 ) )
4	1 2	imbi12d	⊢ ( 𝜑 → ( ( 𝜓 → 𝜒 ) ↔ ( 𝜏 → 𝜂 ) ) )
5	1 3	orbi12d	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ) ↔ ( 𝜏 ∨ 𝜁 ) ) )
6	4 5	anbi12d	⊢ ( 𝜑 → ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜓 ∨ 𝜃 ) ) ↔ ( ( 𝜏 → 𝜂 ) ∧ ( 𝜏 ∨ 𝜁 ) ) ) )
7		dfifp3	⊢ ( if- ( 𝜓 , 𝜒 , 𝜃 ) ↔ ( ( 𝜓 → 𝜒 ) ∧ ( 𝜓 ∨ 𝜃 ) ) )
8		dfifp3	⊢ ( if- ( 𝜏 , 𝜂 , 𝜁 ) ↔ ( ( 𝜏 → 𝜂 ) ∧ ( 𝜏 ∨ 𝜁 ) ) )
9	6 7 8	3bitr4g	⊢ ( 𝜑 → ( if- ( 𝜓 , 𝜒 , 𝜃 ) ↔ if- ( 𝜏 , 𝜂 , 𝜁 ) ) )