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

Theorem con2bii 361
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 notnotb 318 . 2 (𝜓 ↔ ¬ ¬ 𝜓)
2 con2bii.1 . 2 (𝜑 ↔ ¬ 𝜓)
31, 2xchbinxr 338 1 (𝜓 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209
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 210
This theorem is referenced by:  xor3  387  imnan  403  annim  407  pm4.53  983  pm4.55  985  oran  987  nanan  1484  xnor  1504  xorneg  1515  noror  1529  alnex  1783  exnal  1828  exnalimn  1845  2exnexn  1847  equs3OLD  1966  19.3vOLD  1990  nne  3018  rexnal  3232  dfrex2  3233  r2exlem  3294  ddif  4099  dfun2  4221  dfin2  4222  difin  4223  disj4  4391  snnzb  4639  onuninsuci  7549  omopthi  8280  dfsup2  8905  rankxplim3  9307  alephgeom  9506  fin1a2lem7  9826  fin41  9864  reclem2pr  10468  1re  10639  ltnlei  10759  divalglem8  15749  f1omvdco3  18577  elcls  21684  ist1-2  21958  fin1aufil  22543  dchrelbas3  25828  tgdim01  26307  axcontlem12  26775  avril1  28254  creq0  30485  dftr6  33046  sltval2  33223  sltres  33229  nosepeq  33249  nolt02o  33259  nosupbnd2lem1  33275  dfon3  33413  dffun10  33435  brub  33475  bj-bixor  33985  bj-modal4e  34109  con2bii2  34698  wl-dfrexex  34963  wl-dfrexsb  34964  heiborlem1  35197  heiborlem6  35202  heiborlem8  35204  cdleme0nex  37534  wopprc  39891  1nevenALTV  44139
  Copyright terms: Public domain W3C validator