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  382  necon1bbid  2980  r19.9rzv  4498  rexsng  4677  onmindif  6453  iotanul  6518  ondif2  8498  cnpart  15183  sadadd2lem2  16387  isnirred  20226  isreg2  22872  kqcldsat  23228  trufil  23405  itg2cnlem2  25271  issqf  26629  eupth2lem3lem4  29473  pjnorm2  30967  atdmd  31638  atmd2  31640  dfrdg4  34911  dalawlem13  38742  sticksstones1  40950  orddif0suc  42003  infordmin  42268