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

Theorem con2bii 324
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 195 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 323 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 195 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178
This theorem is referenced by:  xor3  348  imnan  413  annim  416  anor  477  pm4.53  480  pm4.55  482  oran  484  3ianor  952  nanan  1299  xnor  1316  xorass  1318  xorneg1  1321  xorneg  1323  alnex  1553  exnal  1584  2exnexn  1591  equs3  1655  19.3v  1678  19.9vOLD  1711  equsexOLD  2004  nne  2606  dfral2  2718  dfrex2  2719  r19.35  2856  ddif  3480  dfun2  3577  dfin2  3578  difin  3579  dfnul2  3631  rab0  3649  disj4  3677  onuninsuci  4821  omopthi  6901  dfsup2  7448  dfsup2OLD  7449  rankxplim3  7806  alephgeom  7964  fin1a2lem7  8287  fin41  8325  reclem2pr  8926  1re  9091  ltnlei  9195  divalglem8  12921  elcls  17138  ist1-2  17412  fin1aufil  17965  dchrelbas3  21023  avril1  21758  dftr6  25374  snnzb  25403  sltval2  25612  sltres  25620  nodenselem4  25640  nodenselem7  25643  nofulllem5  25662  dfon3  25738  dffun10  25760  brub  25800  axcontlem12  25915  heiborlem1  26521  heiborlem6  26526  heiborlem8  26528  wopprc  27102  f1omvdco3  27370  equsexNEW7  29491  cdleme0nex  31088
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 179
  Copyright terms: Public domain W3C validator