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  2979  r19.9rzv  4499  rexsng  4675  onmindif  6475  iotanul  6538  ondif2  8541  cnpart  15280  sadadd2lem2  16488  isnirred  20421  isreg2  23386  kqcldsat  23742  trufil  23919  itg2cnlem2  25798  issqf  27180  eupth2lem3lem4  30251  pjnorm2  31747  atdmd  32418  atmd2  32420  dfrdg4  35953  dalawlem13  39886  sticksstones1  42148  aks6d1c6lem4  42175  orddif0suc  43286  infordmin  43550