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

Theorem con2b 334
Description: Contraposition. Bidirectional version of con2 116. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
con2b

Proof of Theorem con2b
StepHypRef Expression
1 con2 116 . 2
2 con2 116 . 2
31, 2impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  mt2bi  338  pm4.15  581  nic-ax  1506  nic-axALT  1507  alimex  1652  ssconb  3636  disjsn  4090  oneqmini  4934  kmlem4  8554  isprm3  14226  pm13.196a  31321  bnj1171  34056  bnj1176  34061  bnj1204  34068  bnj1388  34089  bnj1523  34127  dfxor5  37790
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