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

Theorem ifpidg 35833
 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 1424 . . 3 if-
21bibi2i 314 . 2 if-
3 dfbi2 632 . . 3
4 imor 413 . . . . 5
5 ordi 872 . . . . 5
6 ancomst 453 . . . . . . 7
7 impexp 447 . . . . . . 7
8 imor 413 . . . . . . . . 9
98imbi2i 313 . . . . . . . 8
10 imor 413 . . . . . . . 8
119, 10bitri 252 . . . . . . 7
126, 7, 113bitrri 275 . . . . . 6
13 imor 413 . . . . . . 7
1413bicomi 205 . . . . . 6
1512, 14anbi12i 701 . . . . 5
164, 5, 153bitri 274 . . . 4
178bicomi 205 . . . . . . . 8
18 df-or 371 . . . . . . . 8
1917, 18anbi12i 701 . . . . . . 7
20 cases2 980 . . . . . . . 8
2120bicomi 205 . . . . . . 7
2219, 21bitri 252 . . . . . 6
2322imbi1i 326 . . . . 5
24 jaob 790 . . . . 5
25 ancomst 453 . . . . . . 7
26 pm5.6 920 . . . . . . 7
2725, 26bitri 252 . . . . . 6
2827anbi2i 698 . . . . 5
2923, 24, 283bitri 274 . . . 4
3016, 29anbi12i 701 . . 3
313, 30bitri 252 . 2
32 ancom 451 . . 3
33 an4 831 . . 3
3432, 33bitri 252 . 2
352, 31, 343bitri 274 1 if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370  if-wif 1420 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 188  df-or 371  df-an 372  df-ifp 1421 This theorem is referenced by:  ifpid3g  35834  ifpid2g  35835  ifpid1g  35836  ifpim23g  35837
 Copyright terms: Public domain W3C validator