Theorem ifpim1g

Description: Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ifpim123g	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) → if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜃 ) ) ) ) )
2		id	⊢ ( 𝜒 → 𝜒 )
3	2	olci	⊢ ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) )
4	3	biantrur	⊢ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) )
5	4	bicomi	⊢ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) )
6		id	⊢ ( 𝜃 → 𝜃 )
7	6	olci	⊢ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜃 ) )
8	7	biantru	⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜃 ) ) ) )
9	8	bicomi	⊢ ( ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜃 ) ) ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) )
10	5 9	anbi12i	⊢ ( ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 → 𝜒 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜃 ) ) ) ) ↔ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ) )
11	1 10	bitri	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜃 ) → if- ( 𝜓 , 𝜒 , 𝜃 ) ) ↔ ( ( ( 𝜓 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 → 𝜃 ) ) ) )