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 ⊢ (𝜓 ↔ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  xor3  385  imnan  405  annim  409  pm4.53  1001  pm4.55  1003  oran  1005  nanan  1523  xnor  1543  xorneg  1553  noror  1563  alnex  1814  exnal  1860  exnalimn  1877  2exnexn  1879  nne  2960  dfrex2  3090  rexnal  3115  r2exlem  3152  ddif  4088  dfun2  4216  dfin2  4217  difin  4218  disj4  4412  snnzb  4679  eqsnuniex  5323  onuninsuci  7840  poxp2  8144  frxp3  8152  omopthi  8654  dif1enlem  9159  dfsup2  9420  rankxplim3  9879  alephgeom  10142  fin1a2lem7  10465  fin41  10503  reclem2pr  11114  ltnlei  11412  divalglem8  16550  f1omvdco3  19643  elcls  23371  ist1-2  23645  fin1aufil  24231  dchrelbas3  27547  ltsval2  27995  ltsres  28001  nosepeq  28024  nolt02o  28034  nogt01o  28035  nosupbnd2lem1  28054  noinfbnd2lem1  28069  madebdaylemlrcut  28267  oncutlt  28632  tgdim01  28952  axcontlem12  29535  avril1  31046  n0nsnel  33093  creq0  33310  axregs  35780  onvf1odlem1  35855  dftr6  36485  dfon3  36624  dffun10  36646  brub  36688  bj-bixor  37431  bj-modal4e  37589  con2bii2  38224  heiborlem1  38713  heiborlem6  38718  heiborlem8  38720  cdleme0nex  41315  aks4d1p7  43101  wopprc  43990  n0nsn2el  48039  1nevenALTV  48733  resinsnALT  49925