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

Theorem con2bii 333
Description: A contraposition inference. (Contributed by NM, 12-Mar-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 205 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 332 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 205 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  xor3  358  imnan  423  annim  426  anor  491  pm4.53  494  pm4.55  496  oran  498  3ianor  999  nanan  1381  xnor  1402  xorassOLD  1405  xorneg1OLD  1413  xorneg  1415  alnex  1661  exnal  1695  2exnexn  1712  equs3  1784  19.3v  1805  nne  2631  rexnal  2880  dfral2OLD  2882  dfrex2  2883  r2exlem  2955  r19.35  2982  ddif  3603  dfun2  3714  dfin2  3715  difin  3716  dfnul2  3769  rab0  3789  disj4  3847  snnzb  4067  onuninsuci  6681  omopthi  7366  dfsup2  7964  rankxplim3  8351  alephgeom  8511  fin1a2lem7  8834  fin41  8872  reclem2pr  9472  1re  9641  ltnlei  9754  divalglem8  14356  f1omvdco3  17032  elcls  20011  ist1-2  20285  fin1aufil  20869  dchrelbas3  24020  tgdim01  24405  axcontlem12  24842  avril1  25736  dftr6  30168  sltval2  30321  sltres  30329  nodenselem4  30349  nodenselem7  30352  nofulllem5  30371  dfon3  30435  dffun10  30457  brub  30497  bj-exnalimn  30991  heiborlem1  31837  heiborlem6  31842  heiborlem8  31844  cdleme0nex  33555  wopprc  35581  1nevenALTV  38200
  Copyright terms: Public domain W3C validator