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  2986  r19.9rzv  4523  rexsng  4698  onmindif  6487  iotanul  6551  ondif2  8558  cnpart  15289  sadadd2lem2  16496  isnirred  20446  isreg2  23406  kqcldsat  23762  trufil  23939  itg2cnlem2  25817  issqf  27197  eupth2lem3lem4  30263  pjnorm2  31759  atdmd  32430  atmd2  32432  dfrdg4  35915  dalawlem13  39840  sticksstones1  42103  aks6d1c6lem4  42130  orddif0suc  43230  infordmin  43494