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 222	. . 3 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))
3	2	con2bid 354	. 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  381  necon1bbid  2972  r19.9rzv  4492  rexsng  4671  onmindif  6447  iotanul  6512  ondif2  8498  cnpart  15185  sadadd2lem2  16390  isnirred  20314  isreg2  23205  kqcldsat  23561  trufil  23738  itg2cnlem2  25616  issqf  26987  eupth2lem3lem4  29956  pjnorm2  31452  atdmd  32123  atmd2  32125  dfrdg4  35419  dalawlem13  39248  sticksstones1  41459  orddif0suc  42532  infordmin  42797