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

Theorem pm5.5 336
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 335 . 2
21bicomd 201 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  imim21b  367  dvelimdf  2077  2sb6rf  2196  elabgt  3243  sbceqal  3383  dffun8  5620  ordiso2  7961  ordtypelem7  7970  cantnf  8133  cantnfOLD  8155  rankonidlem  8267  dfac12lem3  8546  dcomex  8848  indstr2  11189  lublecllem  15618  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  caucfil  21722  isarchiofld  27807  wl-nfimf1  29978  pm10.52  31270  tendoeq2  36500
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 185
  Copyright terms: Public domain W3C validator