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 349
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 348 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 211 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  imim21b  380  dvelimdf  2322  2sb6rf  2439  elabgt  3315  sbceqal  3453  dffun8  5817  ordiso2  8281  ordtypelem7  8290  cantnf  8451  rankonidlem  8552  dfac12lem3  8828  dcomex  9130  indstr2  11602  dfgcd2  15050  lublecllem  16760  tsmsgsum  21700  tsmsres  21705  tsmsxplem1  21714  caucfil  22834  isarchiofld  28982  wl-nfimf1  32316  tendoeq2  34904  elmapintrab  36725  inintabd  36728  cnvcnvintabd  36749  cnvintabd  36752  relexp0eq  36836  ntrkbimka  37180  ntrk0kbimka  37181  pm10.52  37410
  Copyright terms: Public domain W3C validator