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  2964  r19.9rzv  4459  rexsng  4636  onmindif  6414  iotanul  6477  ondif2  8443  cnpart  15182  sadadd2lem2  16396  isnirred  20340  isreg2  23297  kqcldsat  23653  trufil  23830  itg2cnlem2  25696  issqf  27079  eupth2lem3lem4  30210  pjnorm2  31706  atdmd  32377  atmd2  32379  dfrdg4  35932  dalawlem13  39870  sticksstones1  42127  aks6d1c6lem4  42154  orddif0suc  43250  infordmin  43514