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

Theorem con2bii 332
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 202 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 331 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 202 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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 185
This theorem is referenced by:  xor3  357  imnan  422  annim  425  anor  489  pm4.53  492  pm4.55  494  oran  496  3ianor  989  nanan  1344  xnor  1364  xorass  1366  xorneg1  1372  xorneg  1374  alnex  1599  exnal  1633  2exnexn  1650  equs3  1719  19.3v  1740  nne  2642  rexnal  2889  dfral2OLD  2891  dfrex2  2892  r2exlem  2961  r19.35  2988  ddif  3618  dfun2  3715  dfin2  3716  difin  3717  dfnul2  3769  rab0  3788  disj4  3857  snnzb  4075  onuninsuci  6656  omopthi  7304  dfsup2  7900  dfsup2OLD  7901  rankxplim3  8297  alephgeom  8461  fin1a2lem7  8784  fin41  8822  reclem2pr  9424  1re  9593  ltnlei  9703  divalglem8  13930  f1omvdco3  16343  elcls  19440  ist1-2  19714  fin1aufil  20299  dchrelbas3  23378  tgdim01  23763  axcontlem12  24143  avril1  25036  dftr6  29147  sltval2  29384  sltres  29392  nodenselem4  29412  nodenselem7  29415  nofulllem5  29434  dfon3  29510  dffun10  29532  brub  29572  heiborlem1  30275  heiborlem6  30280  heiborlem8  30282  wopprc  30940  bj-exnalimn  33935  cdleme0nex  35717
  Copyright terms: Public domain W3C validator