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 364
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 363 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 226 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  pm5.4  392  imbibi  395  imim21b  399  dvelimdf  2483  r19.35  3123  ceqsralv  3497  elabd2  3632  elabgt  3634  ralsng  4637  dffun8  6553  ordiso2  9465  ordtypelem7  9474  cantnf  9650  rankonidlem  9788  dfac12lem3  10117  dcomex  10419  indstr2  12942  dfgcd2  16594  lublecllem  18404  tsmsgsum  24257  tsmsres  24262  tsmsxplem1  24271  caucfil  25403  isarchiofld  33432  mh-regprimbi  36918  wl-nfimf1  38041  tendoeq2  41410  naddgeoa  43983  elmapintrab  44164  inintabd  44167  cnvcnvintabd  44188  cnvintabd  44191  relexp0eq  44289  ntrkbimka  44626  ntrk0kbimka  44627  pm10.52  44939  ichnfimlem  48067  paireqne  48115
  Copyright terms: Public domain W3C validator