Theorem con2bii 360

Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.)

Hypothesis

Ref	Expression
con2bii.1	⊢ (𝜑 ↔ ¬ 𝜓)

Assertion

Ref	Expression
con2bii	⊢ (𝜓 ↔ ¬ 𝜑)

Proof of Theorem con2bii

Step	Hyp	Ref	Expression
1		notnotb 318	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 338	1 ⊢ (𝜓 ↔ ¬ 𝜑)

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  385  imnan  404  annim  408  pm4.53  1001  pm4.55  1003  oran  1005  nanan  1523  xnor  1543  xorneg  1553  noror  1563  alnex  1811  exnal  1857  exnalimn  1874  2exnexn  1876  nne  2962  dfrex2  3092  rexnal  3117  r2exlem  3154  ddif  4096  dfun2  4224  dfin2  4225  difin  4226  disj4  4420  snnzb  4685  eqsnuniex  5334  onuninsuci  7837  poxp2  8140  frxp3  8148  omopthi  8648  dif1enlem  9145  dfsup2  9405  rankxplim3  9854  alephgeom  10067  fin1a2lem7  10391  fin41  10429  reclem2pr  11034  ltnlei  11332  divalglem8  16459  f1omvdco3  19520  elcls  23211  ist1-2  23485  fin1aufil  24070  dchrelbas3  27383  ltsval2  27801  ltsres  27807  nosepeq  27830  nolt02o  27840  nogt01o  27841  nosupbnd2lem1  27860  noinfbnd2lem1  27875  madebdaylemlrcut  28073  oncutlt  28438  tgdim01  28757  axcontlem12  29306  avril1  30795  n0nsnel  32842  creq0  33062  axregs  35533  onvf1odlem1  35568  dftr6  36224  dfon3  36363  dffun10  36385  brub  36427  bj-bixor  37165  bj-modal4e  37323  con2bii2  37960  heiborlem1  38443  heiborlem6  38448  heiborlem8  38450  cdleme0nex  41045  aks4d1p7  42831  wopprc  43740  n0nsn2el  47745  1nevenALTV  48439  resinsnALT  49634