Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifpidg Structured version   Visualization version   GIF version

Theorem ifpidg 41060
Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
Assertion
Ref Expression
ifpidg ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))

Proof of Theorem ifpidg
StepHypRef Expression
1 dfifp4 1063 . . 3 (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒)))
21bibi2i 337 . 2 ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))))
3 dfbi2 474 . . 3 ((𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ∧ (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)))
4 imor 849 . . . . 5 ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ (¬ 𝜃 ∨ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))))
5 ordi 1002 . . . . 5 ((¬ 𝜃 ∨ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ∧ (¬ 𝜃 ∨ (𝜑𝜒))))
6 ancomst 464 . . . . . . 7 (((𝜑𝜃) → 𝜓) ↔ ((𝜃𝜑) → 𝜓))
7 impexp 450 . . . . . . 7 (((𝜃𝜑) → 𝜓) ↔ (𝜃 → (𝜑𝜓)))
8 imor 849 . . . . . . . . 9 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
98imbi2i 335 . . . . . . . 8 ((𝜃 → (𝜑𝜓)) ↔ (𝜃 → (¬ 𝜑𝜓)))
10 imor 849 . . . . . . . 8 ((𝜃 → (¬ 𝜑𝜓)) ↔ (¬ 𝜃 ∨ (¬ 𝜑𝜓)))
119, 10bitri 274 . . . . . . 7 ((𝜃 → (𝜑𝜓)) ↔ (¬ 𝜃 ∨ (¬ 𝜑𝜓)))
126, 7, 113bitrri 297 . . . . . 6 ((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ↔ ((𝜑𝜃) → 𝜓))
13 imor 849 . . . . . . 7 ((𝜃 → (𝜑𝜒)) ↔ (¬ 𝜃 ∨ (𝜑𝜒)))
1413bicomi 223 . . . . . 6 ((¬ 𝜃 ∨ (𝜑𝜒)) ↔ (𝜃 → (𝜑𝜒)))
1512, 14anbi12i 626 . . . . 5 (((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ∧ (¬ 𝜃 ∨ (𝜑𝜒))) ↔ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))))
164, 5, 153bitri 296 . . . 4 ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))))
178bicomi 223 . . . . . . . 8 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
18 df-or 844 . . . . . . . 8 ((𝜑𝜒) ↔ (¬ 𝜑𝜒))
1917, 18anbi12i 626 . . . . . . 7 (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
20 cases2 1044 . . . . . . . 8 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
2120bicomi 223 . . . . . . 7 (((𝜑𝜓) ∧ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2219, 21bitri 274 . . . . . 6 (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2322imbi1i 349 . . . . 5 ((((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → 𝜃))
24 jaob 958 . . . . 5 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) → 𝜃) ∧ ((¬ 𝜑𝜒) → 𝜃)))
25 ancomst 464 . . . . . . 7 (((¬ 𝜑𝜒) → 𝜃) ↔ ((𝜒 ∧ ¬ 𝜑) → 𝜃))
26 pm5.6 998 . . . . . . 7 (((𝜒 ∧ ¬ 𝜑) → 𝜃) ↔ (𝜒 → (𝜑𝜃)))
2725, 26bitri 274 . . . . . 6 (((¬ 𝜑𝜒) → 𝜃) ↔ (𝜒 → (𝜑𝜃)))
2827anbi2i 622 . . . . 5 ((((𝜑𝜓) → 𝜃) ∧ ((¬ 𝜑𝜒) → 𝜃)) ↔ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))))
2923, 24, 283bitri 296 . . . 4 ((((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))))
3016, 29anbi12i 626 . . 3 (((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ∧ (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)) ↔ ((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))))
313, 30bitri 274 . 2 ((𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))))
32 ancom 460 . . 3 (((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))) ∧ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒)))))
33 an4 652 . . 3 (((((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))) ∧ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
3432, 33bitri 274 . 2 (((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
352, 31, 343bitri 296 1 ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843  if-wif 1059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ifp 1060
This theorem is referenced by:  ifpid3g  41061  ifpid2g  41062  ifpid1g  41063  ifpim23g  41064
  Copyright terms: Public domain W3C validator