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 37314
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 1015 . . 3 (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒)))
21bibi2i 327 . 2 ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))))
3 dfbi2 659 . . 3 ((𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ∧ (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)))
4 imor 428 . . . . 5 ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ (¬ 𝜃 ∨ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))))
5 ordi 907 . . . . 5 ((¬ 𝜃 ∨ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ∧ (¬ 𝜃 ∨ (𝜑𝜒))))
6 ancomst 468 . . . . . . 7 (((𝜑𝜃) → 𝜓) ↔ ((𝜃𝜑) → 𝜓))
7 impexp 462 . . . . . . 7 (((𝜃𝜑) → 𝜓) ↔ (𝜃 → (𝜑𝜓)))
8 imor 428 . . . . . . . . 9 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
98imbi2i 326 . . . . . . . 8 ((𝜃 → (𝜑𝜓)) ↔ (𝜃 → (¬ 𝜑𝜓)))
10 imor 428 . . . . . . . 8 ((𝜃 → (¬ 𝜑𝜓)) ↔ (¬ 𝜃 ∨ (¬ 𝜑𝜓)))
119, 10bitri 264 . . . . . . 7 ((𝜃 → (𝜑𝜓)) ↔ (¬ 𝜃 ∨ (¬ 𝜑𝜓)))
126, 7, 113bitrri 287 . . . . . 6 ((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ↔ ((𝜑𝜃) → 𝜓))
13 imor 428 . . . . . . 7 ((𝜃 → (𝜑𝜒)) ↔ (¬ 𝜃 ∨ (𝜑𝜒)))
1413bicomi 214 . . . . . 6 ((¬ 𝜃 ∨ (𝜑𝜒)) ↔ (𝜃 → (𝜑𝜒)))
1512, 14anbi12i 732 . . . . 5 (((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ∧ (¬ 𝜃 ∨ (𝜑𝜒))) ↔ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))))
164, 5, 153bitri 286 . . . 4 ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))))
178bicomi 214 . . . . . . . 8 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
18 df-or 385 . . . . . . . 8 ((𝜑𝜒) ↔ (¬ 𝜑𝜒))
1917, 18anbi12i 732 . . . . . . 7 (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
20 cases2 992 . . . . . . . 8 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
2120bicomi 214 . . . . . . 7 (((𝜑𝜓) ∧ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2219, 21bitri 264 . . . . . 6 (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2322imbi1i 339 . . . . 5 ((((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → 𝜃))
24 jaob 821 . . . . 5 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) → 𝜃) ∧ ((¬ 𝜑𝜒) → 𝜃)))
25 ancomst 468 . . . . . . 7 (((¬ 𝜑𝜒) → 𝜃) ↔ ((𝜒 ∧ ¬ 𝜑) → 𝜃))
26 pm5.6 950 . . . . . . 7 (((𝜒 ∧ ¬ 𝜑) → 𝜃) ↔ (𝜒 → (𝜑𝜃)))
2725, 26bitri 264 . . . . . 6 (((¬ 𝜑𝜒) → 𝜃) ↔ (𝜒 → (𝜑𝜃)))
2827anbi2i 729 . . . . 5 ((((𝜑𝜓) → 𝜃) ∧ ((¬ 𝜑𝜒) → 𝜃)) ↔ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))))
2923, 24, 283bitri 286 . . . 4 ((((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))))
3016, 29anbi12i 732 . . 3 (((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ∧ (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)) ↔ ((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))))
313, 30bitri 264 . 2 ((𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))))
32 ancom 466 . . 3 (((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))) ∧ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒)))))
33 an4 864 . . 3 (((((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))) ∧ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
3432, 33bitri 264 . 2 (((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
352, 31, 343bitri 286 1 ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  if-wif 1011
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 197  df-or 385  df-an 386  df-ifp 1012
This theorem is referenced by:  ifpid3g  37315  ifpid2g  37316  ifpid1g  37317  ifpim23g  37318
  Copyright terms: Public domain W3C validator