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  2982  r19.9rzv  4427  rexsng  4607  onmindif  6340  iotanul  6396  ondif2  8294  cnpart  14879  sadadd2lem2  16085  isnirred  19857  isreg2  22436  kqcldsat  22792  trufil  22969  itg2cnlem2  24832  issqf  26190  eupth2lem3lem4  28496  pjnorm2  29990  atdmd  30661  atmd2  30663  dfrdg4  34180  dalawlem13  37824  sticksstones1  40030  infordmin  41037