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  990  nanan  1345  xnor  1362  xorass  1364  xorneg1  1370  xorneg  1372  alnex  1598  exnal  1628  2exnexn  1642  equs3  1706  19.3v  1729  nne  2668  rexnal  2912  dfral2OLD  2914  dfrex2  2915  r2exlem  2982  r19.35  3008  ddif  3636  dfun2  3733  dfin2  3734  difin  3735  dfnul2  3787  rab0  3806  disj4  3875  snnzb  4092  onuninsuci  6659  omopthi  7306  dfsup2  7902  dfsup2OLD  7903  rankxplim3  8299  alephgeom  8463  fin1a2lem7  8786  fin41  8824  reclem2pr  9426  1re  9595  ltnlei  9705  divalglem8  13917  f1omvdco3  16280  elcls  19368  ist1-2  19642  fin1aufil  20196  dchrelbas3  23269  tgdim01  23654  axcontlem12  23982  avril1  24875  dftr6  28784  sltval2  29021  sltres  29029  nodenselem4  29049  nodenselem7  29052  nofulllem5  29071  dfon3  29147  dffun10  29169  brub  29209  heiborlem1  29938  heiborlem6  29943  heiborlem8  29945  wopprc  30604  fouriersw  31560  bj-exnalimn  33328  cdleme0nex  35104
  Copyright terms: Public domain W3C validator