MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.5 Structured version   Visualization version   GIF version

Theorem pm5.5 361
Description: Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm5.5 (𝜑 → ((𝜑𝜓) ↔ 𝜓))

Proof of Theorem pm5.5
StepHypRef Expression
1 biimt 360 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 223 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  pm5.4  388  imim21b  394  dvelimdf  2451  r19.35  3105  ceqsralv  3519  elabd2  3669  elabgtOLDOLD  3673  elabg  3676  sbceqalOLD  3857  ralsng  4679  dffun8  6595  ordiso2  9552  ordtypelem7  9561  cantnf  9730  rankonidlem  9865  dfac12lem3  10183  dcomex  10484  indstr2  12966  dfgcd2  16579  lublecllem  18417  tsmsgsum  24162  tsmsres  24167  tsmsxplem1  24176  caucfil  25330  isarchiofld  33326  wl-nfimf1  37506  tendoeq2  40756  naddgeoa  43383  elmapintrab  43565  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  relexp0eq  43690  ntrkbimka  44027  ntrk0kbimka  44028  pm10.52  44360  ichnfimlem  47387  paireqne  47435
  Copyright terms: Public domain W3C validator