Theorem con2bii 349

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

Syntax hints:  ¬ wn 3   ↔ wb 198

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 199

This theorem is referenced by:  xor3  374  imnan  390  annim  394  anor  968  pm4.53  971  pm4.55  973  oran  975  nanan  1559  xnor  1584  xorneg  1594  alnex  1825  exnal  1870  2exnexn  1890  equs3  2006  19.3v  2031  nne  2973  rexnal  3176  dfrex2  3177  r2exlem  3244  r19.35  3270  ddif  3965  dfun2  4086  dfin2  4087  difin  4088  dfnul2OLD  4144  disj4  4251  snnzb  4485  onuninsuci  7320  omopthi  8023  dfsup2  8640  rankxplim3  9043  alephgeom  9240  fin1a2lem7  9565  fin41  9603  reclem2pr  10207  1re  10378  ltnlei  10499  divalglem8  15540  f1omvdco3  18263  elcls  21296  ist1-2  21570  fin1aufil  22155  dchrelbas3  25426  tgdim01  25875  axcontlem12  26341  avril1  27911  dftr6  32242  sltval2  32406  sltres  32412  nosepeq  32432  nolt02o  32442  nosupbnd2lem1  32458  dfon3  32596  dffun10  32618  brub  32658  bj-exnalimn  33197  bj-modal4e  33301  con2bii2  33783  wl-dfrexf  33989  wl-dfrexv  33991  wl-dfrexex  33992  wl-dfrexsb  33993  heiborlem1  34243  heiborlem6  34248  heiborlem8  34250  cdleme0nex  36453  wopprc  38570  1nevenALTV  42641