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 350
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 349 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 213 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  imim21b  381  dvelimdf  2366  2sb6rf  2480  elabgt  3379  sbceqal  3520  dffun8  5954  ordiso2  8461  ordtypelem7  8470  cantnf  8628  rankonidlem  8729  dfac12lem3  9005  dcomex  9307  indstr2  11805  dfgcd2  15310  lublecllem  17035  tsmsgsum  21989  tsmsres  21994  tsmsxplem1  22003  caucfil  23127  isarchiofld  29945  wl-nfimf1  33443  tendoeq2  36379  elmapintrab  38199  inintabd  38202  cnvcnvintabd  38223  cnvintabd  38226  relexp0eq  38310  ntrkbimka  38653  ntrk0kbimka  38654  pm10.52  38881
  Copyright terms: Public domain W3C validator