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 213	. . 3 ⊢ (¬ 𝜓 ↔ 𝜑)
3	2	con1bii 345	. 2 ⊢ (¬ 𝜑 ↔ 𝜓)
4	3	bicomi 213	1 ⊢ (𝜓 ↔ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  xor3  371  imnan  437  annim  440  anor  509  pm4.53  512  pm4.55  514  oran  516  3ianor  1048  nanan  1441  xnor  1458  xorneg  1468  alnex  1697  exnal  1744  2exnexn  1761  equs3  1862  19.3v  1884  nne  2786  rexnal  2978  dfrex2  2979  r2exlem  3041  r19.35  3065  ddif  3704  dfun2  3821  dfin2  3822  difin  3823  dfnul2  3876  rab0OLD  3910  disj4  3977  snnzb  4198  onuninsuci  6932  omopthi  7624  dfsup2  8233  rankxplim3  8627  alephgeom  8788  fin1a2lem7  9111  fin41  9149  reclem2pr  9749  1re  9918  ltnlei  10037  divalglem8  14961  f1omvdco3  17692  elcls  20687  ist1-2  20961  fin1aufil  21546  dchrelbas3  24763  tgdim01  25202  axcontlem12  25655  avril1  26711  dftr6  30893  sltval2  31053  sltres  31061  nodenselem4  31083  nodenselem7  31086  nofulllem5  31105  dfon3  31169  dffun10  31191  brub  31231  bj-exnalimn  31797  bj-modal4e  31892  con2bii2  32356  heiborlem1  32780  heiborlem6  32785  heiborlem8  32787  cdleme0nex  34595  wopprc  36615  1nevenALTV  40140