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 352
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 351 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 214 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  imim21b  383  dvelimdf  2496  2sb6rf  2611  elabgt  3538  sbceqal  3679  dffun8  6123  ordiso2  8653  ordtypelem7  8662  cantnf  8831  rankonidlem  8932  dfac12lem3  9246  dcomex  9548  indstr2  11980  dfgcd2  15476  lublecllem  17187  tsmsgsum  22149  tsmsres  22154  tsmsxplem1  22163  caucfil  23287  isarchiofld  30136  wl-nfimf1  33621  tendoeq2  36549  elmapintrab  38376  inintabd  38379  cnvcnvintabd  38400  cnvintabd  38403  relexp0eq  38487  ntrkbimka  38830  ntrk0kbimka  38831  pm10.52  39058
  Copyright terms: Public domain W3C validator