Theorem ifp1bi

Description: Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020)

	Ref	Expression
Assertion	ifp1bi	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) ↔ if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfbi2	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) ↔ if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) → if- ( 𝜓 , 𝜒 , 𝜃 ) ) ∧ ( if- ( 𝜓 , 𝜒 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜃 ) ) ) )
2		ifpim1g	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) → if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ) )
3	2	biancomi	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) → if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) )
4		ifpim1g	⊢ ( ( if- ( 𝜓 , 𝜒 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜃 ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜃 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜃 ) ) ) )
5	3 4	anbi12i	⊢ ( ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) → if- ( 𝜓 , 𝜒 , 𝜃 ) ) ∧ ( if- ( 𝜓 , 𝜒 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜃 ) ) ) ↔ ( ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜃 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜃 ) ) ) ) )
6		an42	⊢ ( ( ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜃 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜃 ) ) ) ) ↔ ( ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ) )
7	1 5 6	3bitri	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) ↔ if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ) )