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

Theorem ifpdfbi 36087
 Description: Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
Assertion
Ref Expression
ifpdfbi if-

Proof of Theorem ifpdfbi
StepHypRef Expression
1 dfbi2 632 . 2
2 ifpim1 36082 . . . . 5 if-
3 ifpn 1430 . . . . 5 if- if-
42, 3bitr4i 255 . . . 4 if-
5 ifpim2 36085 . . . 4 if-
64, 5anbi12i 701 . . 3 if- if-
7 ifpan23 36073 . . . 4 if- if- if-
8 ancom 451 . . . . . 6
9 truan 1454 . . . . . 6
108, 9bitri 252 . . . . 5
11 truan 1454 . . . . 5
12 ifpbi23 36086 . . . . 5 if- if-
1310, 11, 12mp2an 676 . . . 4 if- if-
147, 13bitri 252 . . 3 if- if- if-
156, 14bitri 252 . 2 if-
161, 15bitri 252 1 if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370  if-wif 1420   wtru 1438 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  df-tru 1440 This theorem is referenced by:  ifpbiidcor  36088  ifpbicor  36089
 Copyright terms: Public domain W3C validator