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

Theorem con2bii 338
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 207 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 337 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 207 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189
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 190
This theorem is referenced by:  xor3  363  imnan  428  annim  431  anor  496  pm4.53  499  pm4.55  501  oran  503  3ianor  1003  nanan  1391  xnor  1410  xorassOLD  1413  xorneg1OLD  1421  xorneg  1423  alnex  1669  exnal  1703  2exnexn  1719  equs3  1796  19.3v  1817  nne  2628  rexnal  2817  dfrex2  2818  r2exlem  2880  r19.35  2905  ddif  3533  dfun2  3646  dfin2  3647  difin  3648  dfnul2  3701  rab0  3721  disj4  3781  snnzb  4005  onuninsuci  6655  omopthi  7345  dfsup2  7945  rankxplim3  8339  alephgeom  8500  fin1a2lem7  8823  fin41  8861  reclem2pr  9460  1re  9629  ltnlei  9742  divalglem8  14391  f1omvdco3  17101  elcls  20100  ist1-2  20374  fin1aufil  20958  dchrelbas3  24178  tgdim01  24563  axcontlem12  25017  avril1  25912  dftr6  30396  sltval2  30549  sltres  30557  nodenselem4  30579  nodenselem7  30582  nofulllem5  30601  dfon3  30665  dffun10  30687  brub  30727  bj-exnalimn  31223  bj-modal4e  31310  con2bii2  31737  heiborlem1  32145  heiborlem6  32150  heiborlem8  32152  cdleme0nex  33858  wopprc  35887  1nevenALTV  38911
  Copyright terms: Public domain W3C validator