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 212 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  imim21b  381  dvelimdf  2323  2sb6rf  2440  elabgt  3316  sbceqal  3454  dffun8  5831  ordiso2  8303  ordtypelem7  8312  cantnf  8473  rankonidlem  8574  dfac12lem3  8850  dcomex  9152  indstr2  11643  dfgcd2  15101  lublecllem  16811  tsmsgsum  21752  tsmsres  21757  tsmsxplem1  21766  caucfil  22889  isarchiofld  29148  wl-nfimf1  32492  tendoeq2  35080  elmapintrab  36901  inintabd  36904  cnvcnvintabd  36925  cnvintabd  36928  relexp0eq  37012  ntrkbimka  37356  ntrk0kbimka  37357  pm10.52  37586
  Copyright terms: Public domain W3C validator