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  1659  exnal  1693  2exnexn  1709  equs3  1785  19.3v  1806  nne  2620  rexnal  2870  dfral2OLD  2872  dfrex2  2873  r2exlem  2945  r19.35  2972  ddif  3597  dfun2  3708  dfin2  3709  difin  3710  dfnul2  3763  rab0  3783  disj4  3843  snnzb  4064  onuninsuci  6681  omopthi  7369  dfsup2  7967  rankxplim3  8360  alephgeom  8520  fin1a2lem7  8843  fin41  8881  reclem2pr  9480  1re  9649  ltnlei  9762  divalglem8  14379  f1omvdco3  17089  elcls  20087  ist1-2  20361  fin1aufil  20945  dchrelbas3  24164  tgdim01  24549  axcontlem12  25003  avril1  25898  dftr6  30397  sltval2  30550  sltres  30558  nodenselem4  30578  nodenselem7  30581  nofulllem5  30600  dfon3  30664  dffun10  30686  brub  30726  bj-exnalimn  31220  con2bii2  31699  heiborlem1  32107  heiborlem6  32112  heiborlem8  32114  cdleme0nex  33825  wopprc  35855  1nevenALTV  38690
  Copyright terms: Public domain W3C validator