Theorem ifpim23g

Description: Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ifpidg	⊢ ( ( ( 𝜑 → 𝜓 ) ↔ if- ( 𝜒 , 𝜓 , ¬ 𝜑 ) ) ↔ ( ( ( ( 𝜒 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜓 ) ) ∧ ( ( ¬ 𝜑 → ( 𝜒 ∨ ( 𝜑 → 𝜓 ) ) ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) ) ) )
2		dfor2	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
3	2	imbi2i	⊢ ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ↔ ( 𝜒 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) )
4		impexp	⊢ ( ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜓 ) ↔ ( 𝜒 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) )
5		ax-1	⊢ ( 𝜓 → ( 𝜑 → 𝜓 ) )
6	5	adantl	⊢ ( ( 𝜒 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) )
7	6	biantrur	⊢ ( ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜓 ) ↔ ( ( ( 𝜒 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜓 ) ) )
8	3 4 7	3bitr2i	⊢ ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ↔ ( ( ( 𝜒 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜓 ) ) )
9		impexp	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( 𝜑 → ( 𝜓 → 𝜒 ) ) )
10		imdi	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )
11		imor	⊢ ( ( 𝜑 → 𝜒 ) ↔ ( ¬ 𝜑 ∨ 𝜒 ) )
12		orcom	⊢ ( ( ¬ 𝜑 ∨ 𝜒 ) ↔ ( 𝜒 ∨ ¬ 𝜑 ) )
13	11 12	bitri	⊢ ( ( 𝜑 → 𝜒 ) ↔ ( 𝜒 ∨ ¬ 𝜑 ) )
14	13	imbi2i	⊢ ( ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) )
15	10 14	bitri	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) )
16	9 15	bitri	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) )
17		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
18	17	olcd	⊢ ( ¬ 𝜑 → ( 𝜒 ∨ ( 𝜑 → 𝜓 ) ) )
19	18	biantrur	⊢ ( ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) ↔ ( ( ¬ 𝜑 → ( 𝜒 ∨ ( 𝜑 → 𝜓 ) ) ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) ) )
20	16 19	bitri	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ↔ ( ( ¬ 𝜑 → ( 𝜒 ∨ ( 𝜑 → 𝜓 ) ) ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) ) )
21	8 20	anbi12i	⊢ ( ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ) ↔ ( ( ( ( 𝜒 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) ) ∧ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → 𝜓 ) ) ∧ ( ( ¬ 𝜑 → ( 𝜒 ∨ ( 𝜑 → 𝜓 ) ) ) ∧ ( ( 𝜑 → 𝜓 ) → ( 𝜒 ∨ ¬ 𝜑 ) ) ) ) )
22		ancom	⊢ ( ( ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ∧ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ) )
23	1 21 22	3bitr2i	⊢ ( ( ( 𝜑 → 𝜓 ) ↔ if- ( 𝜒 , 𝜓 , ¬ 𝜑 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜒 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜓 ) ) ) )