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  2454  r19.35  3108  ceqsralv  3522  elabd2  3670  elabg  3676  sbceqalOLD  3852  ralsng  4675  dffun8  6594  ordiso2  9555  ordtypelem7  9564  cantnf  9733  rankonidlem  9868  dfac12lem3  10186  dcomex  10487  indstr2  12969  dfgcd2  16583  lublecllem  18405  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  caucfil  25317  isarchiofld  33347  wl-nfimf1  37527  tendoeq2  40776  naddgeoa  43407  elmapintrab  43589  inintabd  43592  cnvcnvintabd  43613  cnvintabd  43616  relexp0eq  43714  ntrkbimka  44051  ntrk0kbimka  44052  pm10.52  44384  ichnfimlem  47450  paireqne  47498
  Copyright terms: Public domain W3C validator