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 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  389  imim21b  395  dvelimdf  2447  nfabdwOLD  2926  r19.35  3107  ceqsralv  3511  elabd2  3656  elabgtOLD  3659  elabg  3662  sbceqalOLD  3840  ralsng  4670  dffun8  6565  ordiso2  9492  ordtypelem7  9501  cantnf  9670  rankonidlem  9805  dfac12lem3  10122  dcomex  10424  indstr2  12893  dfgcd2  16470  lublecllem  18295  tsmsgsum  23572  tsmsres  23577  tsmsxplem1  23586  caucfil  24729  isarchiofld  32297  wl-nfimf1  36197  tendoeq2  39448  naddgeoa  41914  elmapintrab  42096  inintabd  42099  cnvcnvintabd  42120  cnvintabd  42123  relexp0eq  42221  ntrkbimka  42558  ntrk0kbimka  42559  pm10.52  42893  ichnfimlem  45901  paireqne  45949
  Copyright terms: Public domain W3C validator