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

Theorem con2bii 323
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
con2bii.1  |-  ( ph  <->  -. 
ps )
Assertion
Ref Expression
con2bii  |-  ( ps  <->  -. 
ph )

Proof of Theorem con2bii
StepHypRef Expression
1 con2bii.1 . . . 4  |-  ( ph  <->  -. 
ps )
21bicomi 194 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 322 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 194 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  xor3  347  imnan  412  annim  415  anor  476  pm4.53  479  pm4.55  481  oran  483  3ianor  951  nanan  1295  xnor  1312  xorass  1314  xorneg1  1317  xorneg  1319  alnex  1549  exnal  1580  2exnexn  1587  equs3  1651  19.3v  1672  19.9vOLD  1704  equsexOLD  1958  nne  2554  dfral2  2661  dfrex2  2662  r19.35  2798  ddif  3422  dfun2  3519  dfin2  3520  difin  3521  dfnul2  3573  rab0  3591  disj4  3619  onuninsuci  4760  omopthi  6836  dfsup2  7382  dfsup2OLD  7383  rankxplim3  7738  alephgeom  7896  fin1a2lem7  8219  fin41  8257  reclem2pr  8858  1re  9023  ltnlei  9125  divalglem8  12847  elcls  17060  ist1-2  17333  fin1aufil  17885  dchrelbas3  20889  avril1  21605  dftr6  25131  sltval2  25334  sltres  25342  nodenselem4  25362  nodenselem7  25365  nofulllem5  25384  dfon3  25456  dffun10  25477  elfuns  25478  axcontlem12  25628  heiborlem1  26211  heiborlem6  26216  heiborlem8  26218  wopprc  26792  f1omvdco3  27061  equsexNEW7  28828  cdleme0nex  30404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator