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 362
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 361 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 222 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  pm5.4  390  imim21b  396  dvelimdf  2448  nfabdwOLD  2932  r19.35  3112  ceqsralv  3484  elabd2  3623  elabgtOLD  3626  elabg  3629  sbceqalOLD  3807  ralsng  4635  dffun8  6530  ordiso2  9452  ordtypelem7  9461  cantnf  9630  rankonidlem  9765  dfac12lem3  10082  dcomex  10384  indstr2  12853  dfgcd2  16428  lublecllem  18250  tsmsgsum  23493  tsmsres  23498  tsmsxplem1  23507  caucfil  24650  isarchiofld  32115  wl-nfimf1  35988  tendoeq2  39240  elmapintrab  41855  inintabd  41858  cnvcnvintabd  41879  cnvintabd  41882  relexp0eq  41980  ntrkbimka  42317  ntrk0kbimka  42318  pm10.52  42652  ichnfimlem  45662  paireqne  45710
  Copyright terms: Public domain W3C validator