Theorem con1bid 358

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.18  384  necon1bbid  2994  r19.9rzv  4460  rexsng  4636  onmindif  6457  iotanul  6518  ondif2  8510  cnpart  15407  sadadd2lem2  16620  isnirred  20650  isreg2  23695  kqcldsat  24052  trufil  24229  itg2cnlem2  26083  issqf  27463  eupth2lem3lem4  30832  pjnorm2  32329  atdmd  33000  atmd2  33002  dfrdg4  36715  nmulle  36966  qdiffALT  38250  dalawlem13  40941  sticksstones1  43197  aks6d1c6lem4  43224  orddif0suc  44270  infordmin  44533  prmringnzring  49434