Theorem con1bid 356

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 355	. 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  383  necon1bbid  2981  r19.9rzv  4500  rexsng  4679  onmindif  6457  iotanul  6522  ondif2  8502  cnpart  15187  sadadd2lem2  16391  isnirred  20234  isreg2  22881  kqcldsat  23237  trufil  23414  itg2cnlem2  25280  issqf  26640  eupth2lem3lem4  29484  pjnorm2  30980  atdmd  31651  atmd2  31653  dfrdg4  34923  dalawlem13  38754  sticksstones1  40962  orddif0suc  42018  infordmin  42283