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

Theorem con2bii 332
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.)
Hypothesis
Ref Expression
con2bii.1
Assertion
Ref Expression
con2bii

Proof of Theorem con2bii
StepHypRef Expression
1 con2bii.1 . . . 4
21bicomi 202 . . 3
32con1bii 331 . 2
43bicomi 202 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
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  1365  xorass  1367  xorneg1  1373  xorneg  1375  alnex  1614  exnal  1648  2exnexn  1665  equs3  1734  19.3v  1755  nne  2658  rexnal  2905  dfral2OLD  2907  dfrex2  2908  r2exlem  2977  r19.35  3004  ddif  3635  dfun2  3732  dfin2  3733  difin  3734  dfnul2  3786  rab0  3806  disj4  3875  snnzb  4094  onuninsuci  6675  omopthi  7325  dfsup2  7922  dfsup2OLD  7923  rankxplim3  8320  alephgeom  8484  fin1a2lem7  8807  fin41  8845  reclem2pr  9447  1re  9616  ltnlei  9726  divalglem8  14058  f1omvdco3  16474  elcls  19574  ist1-2  19848  fin1aufil  20433  dchrelbas3  23513  tgdim01  23898  axcontlem12  24278  avril1  25171  dftr6  29179  sltval2  29416  sltres  29424  nodenselem4  29444  nodenselem7  29447  nofulllem5  29466  dfon3  29542  dffun10  29564  brub  29604  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  wopprc  30972  bj-exnalimn  34221  cdleme0nex  36015
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
  Copyright terms: Public domain W3C validator