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  2485  2sb6rf  2600  elabgt  3498  sbceqal  3639  dffun8  6057  ordiso2  8576  ordtypelem7  8585  cantnf  8754  rankonidlem  8855  dfac12lem3  9169  dcomex  9471  indstr2  11971  dfgcd2  15467  lublecllem  17192  tsmsgsum  22158  tsmsres  22163  tsmsxplem1  22172  caucfil  23296  isarchiofld  30153  wl-nfimf1  33644  tendoeq2  36580  elmapintrab  38405  inintabd  38408  cnvcnvintabd  38429  cnvintabd  38432  relexp0eq  38516  ntrkbimka  38859  ntrk0kbimka  38860  pm10.52  39087
  Copyright terms: Public domain W3C validator