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  1673  19.9vOLD  1706  equsexOLD  1970  nne  2575  dfral2  2682  dfrex2  2683  r19.35  2819  ddif  3443  dfun2  3540  dfin2  3541  difin  3542  dfnul2  3594  rab0  3612  disj4  3640  onuninsuci  4783  omopthi  6863  dfsup2  7409  dfsup2OLD  7410  rankxplim3  7765  alephgeom  7923  fin1a2lem7  8246  fin41  8284  reclem2pr  8885  1re  9050  ltnlei  9154  divalglem8  12879  elcls  17096  ist1-2  17369  fin1aufil  17921  dchrelbas3  20979  avril1  21714  dftr6  25325  sltval2  25528  sltres  25536  nodenselem4  25556  nodenselem7  25559  nofulllem5  25578  dfon3  25650  dffun10  25671  elfuns  25672  axcontlem12  25822  heiborlem1  26414  heiborlem6  26419  heiborlem8  26421  wopprc  26995  f1omvdco3  27264  equsexNEW7  29200  cdleme0nex  30776
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