Theorem con1bid 357

Description: A contraposition deduction. (Contributed by NM, 9-Oct-1999.)

Hypothesis

Ref	Expression
con1bid.1	⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒))

Assertion

Ref	Expression
con1bid	⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))

Proof of Theorem con1bid

Step	Hyp	Ref	Expression
1		con1bid.1	. . . 4 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒))
2	1	bicomd 225	. . 3 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))
3	2	con2bid 356	. 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))
4	3	bicomd 225	1 ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pm5.18  383  necon1bbid  2975  r19.9rzv  4436  rexsng  4611  onmindif  6408  iotanul  6469  ondif2  8431  cnpart  15197  sadadd2lem2  16414  isnirred  20395  isreg2  23364  kqcldsat  23720  trufil  23897  itg2cnlem2  25751  issqf  27121  eupth2lem3lem4  30323  pjnorm2  31820  atdmd  32491  atmd2  32493  dfrdg4  36194  qdiffALT  37703  dalawlem13  40390  sticksstones1  42646  aks6d1c6lem4  42673  orddif0suc  43728  infordmin  43991