Theorem ifpid1g

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

	Ref	Expression
Assertion	ifpid1g	⊢ ( ( 𝜑 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( 𝜒 → 𝜑 ) ∧ ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ifpidg	⊢ ( ( 𝜑 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ∧ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
2		ancom	⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ∧ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) ) ) ) ↔ ( ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ∧ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ) ) )
3		pm4.25	⊢ ( 𝜑 ↔ ( 𝜑 ∨ 𝜑 ) )
4	3	imbi2i	⊢ ( ( 𝜒 → 𝜑 ) ↔ ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) )
5		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) )
6	5	biantru	⊢ ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ↔ ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) ) ) )
7	4 6	bitr2i	⊢ ( ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( 𝜒 → 𝜑 ) )
8		pm4.24	⊢ ( 𝜑 ↔ ( 𝜑 ∧ 𝜑 ) )
9	8	imbi1i	⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) )
10		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
11	10	biantrur	⊢ ( ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ∧ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ) )
12	9 11	bitr2i	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ∧ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ) ↔ ( 𝜑 → 𝜓 ) )
13	7 12	anbi12i	⊢ ( ( ( ( 𝜒 → ( 𝜑 ∨ 𝜑 ) ) ∧ ( 𝜑 → ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) ∧ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 ) ) ) ↔ ( ( 𝜒 → 𝜑 ) ∧ ( 𝜑 → 𝜓 ) ) )
14	1 2 13	3bitri	⊢ ( ( 𝜑 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( 𝜒 → 𝜑 ) ∧ ( 𝜑 → 𝜓 ) ) )