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

Theorem con34b 292
Description: Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
con34b

Proof of Theorem con34b
StepHypRef Expression
1 con3 134 . 2
2 ax-3 8 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  mtt  339  pm4.14  578  r19.23v  2937  raldifsni  4160  dff14a  6177  weniso  6250  dfom2  6702  dfsup2  7922  wemapsolem  7996  pwfseqlem3  9059  indstr  11179  rpnnen2  13959  algcvgblem  14206  isirred2  17350  isdomn2  17948  ist0-3  19846  mdegleb  22464  dchrelbas4  23518  toslublem  27655  tosglblem  27657  tsbi3  30542  isdomn3  31164  conss34  31351  aacllem  33216
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