Theorem con1bid 354

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pm5.18  380  necon1bbid  2978  r19.9rzv  4498  rexsng  4677  onmindif  6455  iotanul  6520  ondif2  8504  cnpart  15191  sadadd2lem2  16395  isnirred  20311  isreg2  23101  kqcldsat  23457  trufil  23634  itg2cnlem2  25512  issqf  26876  eupth2lem3lem4  29751  pjnorm2  31247  atdmd  31918  atmd2  31920  dfrdg4  35227  dalawlem13  39057  sticksstones1  41268  orddif0suc  42320  infordmin  42585