MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2bii 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 5    <-> wb 178
This theorem is referenced by:  xor3  348  imnan  413  annim  416  anor  477  pm4.53  480  pm4.55  482  oran  484  3ianor  954  nanan  1294  xnor  1302  xorass  1304  xorneg1  1307  xorneg  1309  alnex  1569  exnal  1572  2exnexn  1578  equs3  1627  equsex  1853  nne  2425  dfral2  2530  dfrex2  2531  r19.35  2662  ddif  3283  dfun2  3379  dfin2  3380  difin  3381  dfnul2  3432  rab0  3450  disj4  3478  onuninsuci  4603  omopthi  6623  dfsup2  7163  dfsup2OLD  7164  rankxplim3  7519  alephgeom  7677  ominf4  7906  fin1a2lem7  8000  fin41  8038  reclem2pr  8640  1re  8805  ltnlei  8907  divalglem8  12561  elcls  16772  ist1-2  17037  fin1aufil  17589  dchrelbas3  20439  avril1  20796  dftr6  23478  sltval2  23678  sltres  23686  axdenselem4  23707  axdenselem7  23710  axfelem15  23729  axfelem18  23732  axfelem22  23736  dfon3  23808  elfuns  23829  axcontlem12  23978  tnf  24318  boxeq  24353  heiborlem1  25902  heiborlem6  25907  heiborlem8  25909  wopprc  26490  f1omvdco3  26759  19.8vK  28171  equsexv-x12  28280  cdleme0nex  29646
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator