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  2972  r19.9rzv  4460  rexsng  4635  onmindif  6421  iotanul  6482  ondif2  8441  cnpart  15177  sadadd2lem2  16391  isnirred  20373  isreg2  23338  kqcldsat  23694  trufil  23871  itg2cnlem2  25736  issqf  27119  eupth2lem3lem4  30324  pjnorm2  31821  atdmd  32492  atmd2  32494  dfrdg4  36173  dalawlem13  40288  sticksstones1  42545  aks6d1c6lem4  42572  orddif0suc  43654  infordmin  43917