Metamath Proof Explorer

Theorem ifpidg

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

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

Proof

Step Hyp Ref Expression
1 dfifp4 ⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) )
2 1 bibi2i ⊢ ( ( 𝜃 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( 𝜃 ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) )
3 dfbi2 ⊢ ( ( 𝜃 ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( 𝜃 → ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) → 𝜃 ) ) )
4 imor ⊢ ( ( 𝜃 → ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ¬ 𝜃 ∨ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) )
5 ordi ⊢ ( ( ¬ 𝜃 ∨ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( ¬ 𝜃 ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ∧ ( ¬ 𝜃 ∨ ( 𝜑 ∨ 𝜒 ) ) ) )
6 ancomst ⊢ ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ↔ ( ( 𝜃 ∧ 𝜑 ) → 𝜓 ) )
7 impexp ⊢ ( ( ( 𝜃 ∧ 𝜑 ) → 𝜓 ) ↔ ( 𝜃 → ( 𝜑 → 𝜓 ) ) )
8 imor ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∨ 𝜓 ) )
9 8 imbi2i ⊢ ( ( 𝜃 → ( 𝜑 → 𝜓 ) ) ↔ ( 𝜃 → ( ¬ 𝜑 ∨ 𝜓 ) ) )
10 imor ⊢ ( ( 𝜃 → ( ¬ 𝜑 ∨ 𝜓 ) ) ↔ ( ¬ 𝜃 ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) )
11 9 10 bitri ⊢ ( ( 𝜃 → ( 𝜑 → 𝜓 ) ) ↔ ( ¬ 𝜃 ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) )
12 6 7 11 3bitrri ⊢ ( ( ¬ 𝜃 ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ↔ ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) )
13 imor ⊢ ( ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ↔ ( ¬ 𝜃 ∨ ( 𝜑 ∨ 𝜒 ) ) )
14 13 bicomi ⊢ ( ( ¬ 𝜃 ∨ ( 𝜑 ∨ 𝜒 ) ) ↔ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) )
15 12 14 anbi12i ⊢ ( ( ( ¬ 𝜃 ∨ ( ¬ 𝜑 ∨ 𝜓 ) ) ∧ ( ¬ 𝜃 ∨ ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) )
16 4 5 15 3bitri ⊢ ( ( 𝜃 → ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) )
17 8 bicomi ⊢ ( ( ¬ 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 → 𝜓 ) )
18 df-or ⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( ¬ 𝜑 → 𝜒 ) )
19 17 18 anbi12i ⊢ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
20 cases2 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
21 20 bicomi ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
22 19 21 bitri ⊢ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
23 22 imbi1i ⊢ ( ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) → 𝜃 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜃 ) )
24 jaob ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜃 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜃 ) ) )
25 ancomst ⊢ ( ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜃 ) ↔ ( ( 𝜒 ∧ ¬ 𝜑 ) → 𝜃 ) )
26 pm5.6 ⊢ ( ( ( 𝜒 ∧ ¬ 𝜑 ) → 𝜃 ) ↔ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) )
27 25 26 bitri ⊢ ( ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜃 ) ↔ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) )
28 27 anbi2i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( ( ¬ 𝜑 ∧ 𝜒 ) → 𝜃 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) )
29 23 24 28 3bitri ⊢ ( ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) → 𝜃 ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) )
30 16 29 anbi12i ⊢ ( ( ( 𝜃 → ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) → 𝜃 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) ) )
31 3 30 bitri ⊢ ( ( 𝜃 ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) ) )
32 ancom ⊢ ( ( ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
33 an4 ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
34 32 33 bitri ⊢ ( ( ( ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ∧ ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ) )
35 2 31 34 3bitri ⊢ ( ( 𝜃 ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) ) ↔ ( ( ( ( 𝜑 ∧ 𝜓 ) → 𝜃 ) ∧ ( ( 𝜑 ∧ 𝜃 ) → 𝜓 ) ) ∧ ( ( 𝜒 → ( 𝜑 ∨ 𝜃 ) ) ∧ ( 𝜃 → ( 𝜑 ∨ 𝜒 ) ) ) ) )