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

Theorem ifpidg 36855
 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 1010 . . 3 (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒)))
21bibi2i 326 . 2 ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))))
3 dfbi2 658 . . 3 ((𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ∧ (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)))
4 imor 427 . . . . 5 ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ (¬ 𝜃 ∨ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))))
5 ordi 904 . . . . 5 ((¬ 𝜃 ∨ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ∧ (¬ 𝜃 ∨ (𝜑𝜒))))
6 ancomst 467 . . . . . . 7 (((𝜑𝜃) → 𝜓) ↔ ((𝜃𝜑) → 𝜓))
7 impexp 461 . . . . . . 7 (((𝜃𝜑) → 𝜓) ↔ (𝜃 → (𝜑𝜓)))
8 imor 427 . . . . . . . . 9 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
98imbi2i 325 . . . . . . . 8 ((𝜃 → (𝜑𝜓)) ↔ (𝜃 → (¬ 𝜑𝜓)))
10 imor 427 . . . . . . . 8 ((𝜃 → (¬ 𝜑𝜓)) ↔ (¬ 𝜃 ∨ (¬ 𝜑𝜓)))
119, 10bitri 263 . . . . . . 7 ((𝜃 → (𝜑𝜓)) ↔ (¬ 𝜃 ∨ (¬ 𝜑𝜓)))
126, 7, 113bitrri 286 . . . . . 6 ((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ↔ ((𝜑𝜃) → 𝜓))
13 imor 427 . . . . . . 7 ((𝜃 → (𝜑𝜒)) ↔ (¬ 𝜃 ∨ (𝜑𝜒)))
1413bicomi 213 . . . . . 6 ((¬ 𝜃 ∨ (𝜑𝜒)) ↔ (𝜃 → (𝜑𝜒)))
1512, 14anbi12i 729 . . . . 5 (((¬ 𝜃 ∨ (¬ 𝜑𝜓)) ∧ (¬ 𝜃 ∨ (𝜑𝜒))) ↔ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))))
164, 5, 153bitri 285 . . . 4 ((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))))
178bicomi 213 . . . . . . . 8 ((¬ 𝜑𝜓) ↔ (𝜑𝜓))
18 df-or 384 . . . . . . . 8 ((𝜑𝜒) ↔ (¬ 𝜑𝜒))
1917, 18anbi12i 729 . . . . . . 7 (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
20 cases2 1005 . . . . . . . 8 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
2120bicomi 213 . . . . . . 7 (((𝜑𝜓) ∧ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2219, 21bitri 263 . . . . . 6 (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2322imbi1i 338 . . . . 5 ((((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → 𝜃))
24 jaob 818 . . . . 5 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) → 𝜃) ∧ ((¬ 𝜑𝜒) → 𝜃)))
25 ancomst 467 . . . . . . 7 (((¬ 𝜑𝜒) → 𝜃) ↔ ((𝜒 ∧ ¬ 𝜑) → 𝜃))
26 pm5.6 949 . . . . . . 7 (((𝜒 ∧ ¬ 𝜑) → 𝜃) ↔ (𝜒 → (𝜑𝜃)))
2725, 26bitri 263 . . . . . 6 (((¬ 𝜑𝜒) → 𝜃) ↔ (𝜒 → (𝜑𝜃)))
2827anbi2i 726 . . . . 5 ((((𝜑𝜓) → 𝜃) ∧ ((¬ 𝜑𝜒) → 𝜃)) ↔ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))))
2923, 24, 283bitri 285 . . . 4 ((((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃) ↔ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))))
3016, 29anbi12i 729 . . 3 (((𝜃 → ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ∧ (((¬ 𝜑𝜓) ∧ (𝜑𝜒)) → 𝜃)) ↔ ((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))))
313, 30bitri 263 . 2 ((𝜃 ↔ ((¬ 𝜑𝜓) ∧ (𝜑𝜒))) ↔ ((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))))
32 ancom 465 . . 3 (((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))) ∧ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒)))))
33 an4 861 . . 3 (((((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃))) ∧ (((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
3432, 33bitri 263 . 2 (((((𝜑𝜃) → 𝜓) ∧ (𝜃 → (𝜑𝜒))) ∧ (((𝜑𝜓) → 𝜃) ∧ (𝜒 → (𝜑𝜃)))) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
352, 31, 343bitri 285 1 ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑𝜓) → 𝜃) ∧ ((𝜑𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑𝜃)) ∧ (𝜃 → (𝜑𝜒)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383  if-wif 1006 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 196  df-or 384  df-an 385  df-ifp 1007 This theorem is referenced by:  ifpid3g  36856  ifpid2g  36857  ifpid1g  36858  ifpim23g  36859
 Copyright terms: Public domain W3C validator