Theorem con2bii 358

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 315	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 335	1 ⊢ (𝜓 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  xor3  384  imnan  400  annim  404  pm4.53  983  pm4.55  985  oran  987  nanan  1488  xnor  1508  xorneg  1519  noror  1531  alnex  1784  exnal  1829  exnalimn  1846  2exnexn  1848  nne  2947  rexnal  3169  dfrex2  3170  r2exlem  3231  ddif  4071  dfun2  4193  dfin2  4194  difin  4195  disj4  4392  snnzb  4654  eqsnuniex  5283  onuninsuci  7687  omopthi  8491  dif1enlem  8943  dfsup2  9203  rankxplim3  9639  alephgeom  9838  fin1a2lem7  10162  fin41  10200  reclem2pr  10804  1re  10975  ltnlei  11096  divalglem8  16109  f1omvdco3  19057  elcls  22224  ist1-2  22498  fin1aufil  23083  dchrelbas3  26386  tgdim01  26868  axcontlem12  27343  avril1  28827  creq0  31070  dftr6  33718  poxp2  33790  poxp3  33796  frxp3  33797  sltval2  33859  sltres  33865  nosepeq  33888  nolt02o  33898  nogt01o  33899  nosupbnd2lem1  33918  noinfbnd2lem1  33933  madebdaylemlrcut  34079  dfon3  34194  dffun10  34216  brub  34256  bj-bixor  34773  bj-modal4e  34897  con2bii2  35504  heiborlem1  35969  heiborlem6  35974  heiborlem8  35976  cdleme0nex  38304  aks4d1p7  40091  wopprc  40852  1nevenALTV  45143