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  2964  r19.9rzv  4463  rexsng  4640  onmindif  6426  iotanul  6489  ondif2  8466  cnpart  15206  sadadd2lem2  16420  isnirred  20329  isreg2  23264  kqcldsat  23620  trufil  23797  itg2cnlem2  25663  issqf  27046  eupth2lem3lem4  30160  pjnorm2  31656  atdmd  32327  atmd2  32329  dfrdg4  35939  dalawlem13  39877  sticksstones1  42134  aks6d1c6lem4  42161  orddif0suc  43257  infordmin  43521