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  4446  rexsng  4621  onmindif  6413  iotanul  6474  ondif2  8432  cnpart  15197  sadadd2lem2  16414  isnirred  20395  isreg2  23356  kqcldsat  23712  trufil  23889  itg2cnlem2  25743  issqf  27117  eupth2lem3lem4  30320  pjnorm2  31817  atdmd  32488  atmd2  32490  dfrdg4  36153  dalawlem13  40347  sticksstones1  42603  aks6d1c6lem4  42630  orddif0suc  43718  infordmin  43981