Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.5 Structured version   Visualization version   GIF version

Theorem pm5.5 365
 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 364 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21bicomd 226 1 (𝜑 → ((𝜑𝜓) ↔ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  pm5.4  393  imim21b  398  dvelimdf  2460  nfabdw  2976  elabgt  3609  sbceqal  3783  dffun8  6357  ordiso2  8978  ordtypelem7  8987  cantnf  9155  rankonidlem  9256  dfac12lem3  9571  dcomex  9873  indstr2  12332  dfgcd2  15901  lublecllem  17607  tsmsgsum  22782  tsmsres  22787  tsmsxplem1  22796  caucfil  23925  isarchiofld  30987  wl-nfimf1  34998  tendoeq2  38137  elmapintrab  40363  inintabd  40366  cnvcnvintabd  40387  cnvintabd  40390  relexp0eq  40489  ntrkbimka  40828  ntrk0kbimka  40829  pm10.52  41156  ichnfimlem  44064  paireqne  44112
 Copyright terms: Public domain W3C validator