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

Step	Hyp	Ref	Expression
1		con2bii.1	. . . 4 ⊢ (𝜑 ↔ ¬ 𝜓)
2	1	bicomi 214	. . 3 ⊢ (¬ 𝜓 ↔ 𝜑)
3	2	con1bii 345	. 2 ⊢ (¬ 𝜑 ↔ 𝜓)
4	3	bicomi 214	1 ⊢ (𝜓 ↔ ¬ 𝜑)

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  386  annim  390  anor  957  pm4.53  960  pm4.55  962  oran  964  3ianorOLD  1098  nanan  1597  xnor  1614  xorneg  1624  alnex  1854  exnal  1902  2exnexn  1922  equs3  2044  19.3v  2066  nne  2947  rexnal  3143  dfrex2  3144  r2exlem  3207  r19.35  3232  ddif  3894  dfun2  4009  dfin2  4010  difin  4011  dfnul2  4066  disj4  4170  snnzb  4391  onuninsuci  7188  omopthi  7892  dfsup2  8507  rankxplim3  8909  alephgeom  9106  fin1a2lem7  9431  fin41  9469  reclem2pr  10073  1re  10242  ltnlei  10361  divalglem8  15332  f1omvdco3  18077  elcls  21099  ist1-2  21373  fin1aufil  21957  dchrelbas3  25185  tgdim01  25624  axcontlem12  26077  avril1  27662  dftr6  31979  sltval2  32147  sltres  32153  nosepeq  32173  nolt02o  32183  nosupbnd2lem1  32199  dfon3  32337  dffun10  32359  brub  32399  bj-exnalimn  32948  bj-modal4e  33043  con2bii2  33518  heiborlem1  33943  heiborlem6  33948  heiborlem8  33950  cdleme0nex  36100  wopprc  38124  1nevenALTV  42131