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  1852  nne  2416  dfral2  2519  dfrex2  2520  r19.35  2649  ddif  3222  dfun2  3311  dfin2  3312  difin  3313  dfnul2  3364  rab0  3382  disj4  3410  onuninsuci  4522  omopthi  6541  dfsup2  7079  dfsup2OLD  7080  rankxplim3  7435  alephgeom  7593  ominf4  7822  fin1a2lem7  7916  fin41  7954  reclem2pr  8552  1re  8717  ltnlei  8819  divalglem8  12473  elcls  16642  ist1-2  16907  fin1aufil  17459  dchrelbas3  20309  avril1  20666  dftr6  23277  sltval2  23477  sltres  23485  axdenselem4  23506  axdenselem7  23509  axfelem15  23528  axfelem18  23531  axfelem22  23535  dfon3  23607  elfuns  23628  axcontlem12  23777  tnf  24117  boxeq  24152  heiborlem1  25701  heiborlem6  25706  heiborlem8  25708  wopprc  26289  f1omvdco3  26558  equsexv-x12  27802  cdleme0nex  29168
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