Theorem ifpimimb

Description: Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

	Ref	Expression
Assertion	ifpimimb	⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfifp2	⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) )
2		imor	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( ¬ 𝜑 ∨ ( 𝜓 → 𝜒 ) ) )
3		pm4.8	⊢ ( ( 𝜑 → ¬ 𝜑 ) ↔ ¬ 𝜑 )
4	3	bicomi	⊢ ( ¬ 𝜑 ↔ ( 𝜑 → ¬ 𝜑 ) )
5	4	orbi1i	⊢ ( ( ¬ 𝜑 ∨ ( 𝜓 → 𝜒 ) ) ↔ ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) )
6		id	⊢ ( 𝜑 → 𝜑 )
7	6	orci	⊢ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) )
8	7	biantru	⊢ ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ↔ ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) )
9	2 5 8	3bitri	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) )
10		pm4.64	⊢ ( ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ↔ ( 𝜑 ∨ ( 𝜃 → 𝜏 ) ) )
11		pm4.81	⊢ ( ( ¬ 𝜑 → 𝜑 ) ↔ 𝜑 )
12	11	bicomi	⊢ ( 𝜑 ↔ ( ¬ 𝜑 → 𝜑 ) )
13	12	orbi1i	⊢ ( ( 𝜑 ∨ ( 𝜃 → 𝜏 ) ) ↔ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) )
14	6	orci	⊢ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) )
15	14	biantrur	⊢ ( ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ↔ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) )
16	10 13 15	3bitri	⊢ ( ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ↔ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) )
17	9 16	anbi12i	⊢ ( ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 → 𝜏 ) ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) ) )
18		ifpim123g	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) ) )
19	18	bicomi	⊢ ( ( ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
20	1 17 19	3bitri	⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )