Theorem con1bid 355

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 223	. . 3 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))
3	2	con2bid 354	. 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))
4	3	bicomd 223	1 ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))

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

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 207

This theorem is referenced by:  pm5.18  381  necon1bbid  2971  r19.9rzv  4445  rexsng  4620  onmindif  6417  iotanul  6478  ondif2  8437  cnpart  15202  sadadd2lem2  16419  isnirred  20400  isreg2  23342  kqcldsat  23698  trufil  23875  itg2cnlem2  25729  issqf  27099  eupth2lem3lem4  30301  pjnorm2  31798  atdmd  32469  atmd2  32471  dfrdg4  36133  qdiffALT  37642  dalawlem13  40329  sticksstones1  42585  aks6d1c6lem4  42612  orddif0suc  43696  infordmin  43959