Theorem con2bii 357

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 314	. 2 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
2		con2bii.1	. 2 ⊢ (𝜑 ↔ ¬ 𝜓)
3	1, 2	xchbinxr 334	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  383  imnan  399  annim  403  pm4.53  982  pm4.55  984  oran  986  nanan  1485  xnor  1505  xorneg  1516  noror  1530  alnex  1785  exnal  1830  exnalimn  1847  2exnexn  1849  nne  2946  rexnal  3165  dfrex2  3166  r2exlem  3230  ddif  4067  dfun2  4190  dfin2  4191  difin  4192  disj4  4389  snnzb  4651  eqsnuniex  5278  onuninsuci  7662  omopthi  8451  dif1enlem  8905  dfsup2  9133  rankxplim3  9570  alephgeom  9769  fin1a2lem7  10093  fin41  10131  reclem2pr  10735  1re  10906  ltnlei  11026  divalglem8  16037  f1omvdco3  18972  elcls  22132  ist1-2  22406  fin1aufil  22991  dchrelbas3  26291  tgdim01  26772  axcontlem12  27246  avril1  28728  creq0  30972  dftr6  33624  poxp2  33717  poxp3  33723  frxp3  33724  sltval2  33786  sltres  33792  nosepeq  33815  nolt02o  33825  nogt01o  33826  nosupbnd2lem1  33845  noinfbnd2lem1  33860  madebdaylemlrcut  34006  dfon3  34121  dffun10  34143  brub  34183  bj-bixor  34700  bj-modal4e  34824  con2bii2  35431  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  cdleme0nex  38231  aks4d1p7  40019  wopprc  40768  1nevenALTV  45031