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

Theorem con2bii 346
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 214 . . 3 𝜓𝜑)
32con1bii 345 . 2 𝜑𝜓)
43bicomi 214 1 (𝜓 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  xor3  371  imnan  437  annim  440  anor  509  pm4.53  512  pm4.55  514  oran  516  3ianorOLD  1076  nanan  1489  xnor  1506  xorneg  1516  alnex  1746  exnal  1794  2exnexn  1812  equs3  1932  19.3v  1954  nne  2827  rexnal  3024  dfrex2  3025  r2exlem  3088  r19.35  3113  ddif  3775  dfun2  3892  dfin2  3893  difin  3894  dfnul2  3950  rab0OLD  3989  disj4  4058  snnzb  4286  onuninsuci  7082  omopthi  7782  dfsup2  8391  rankxplim3  8782  alephgeom  8943  fin1a2lem7  9266  fin41  9304  reclem2pr  9908  1re  10077  ltnlei  10196  divalglem8  15170  f1omvdco3  17915  elcls  20925  ist1-2  21199  fin1aufil  21783  dchrelbas3  25008  tgdim01  25447  axcontlem12  25900  avril1  27449  dftr6  31766  sltval2  31934  sltres  31940  nosepeq  31960  nolt02o  31970  nosupbnd2lem1  31986  dfon3  32124  dffun10  32146  brub  32186  bj-exnalimn  32735  bj-modal4e  32830  con2bii2  33310  heiborlem1  33740  heiborlem6  33745  heiborlem8  33747  cdleme0nex  35895  wopprc  37914  1nevenALTV  41927
  Copyright terms: Public domain W3C validator