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  7318  omopthi  8021  dfsup2  8638  rankxplim3  9041  alephgeom  9238  fin1a2lem7  9563  fin41  9601  reclem2pr  10205  1re  10376  ltnlei  10497  divalglem8  15530  f1omvdco3  18252  elcls  21285  ist1-2  21559  fin1aufil  22144  dchrelbas3  25415  tgdim01  25858  axcontlem12  26324  avril1  27894  dftr6  32234  sltval2  32398  sltres  32404  nosepeq  32424  nolt02o  32434  nosupbnd2lem1  32450  dfon3  32588  dffun10  32610  brub  32650  bj-exnalimn  33189  bj-modal4e  33293  con2bii2  33776  wl-dfrexf  33980  wl-dfrexv  33982  wl-dfrexex  33983  wl-dfrexsb  33984  heiborlem1  34234  heiborlem6  34239  heiborlem8  34241  cdleme0nex  36444  wopprc  38556  1nevenALTV  42627