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  2983  r19.9rzv  4430  rexsng  4610  onmindif  6355  iotanul  6411  ondif2  8332  cnpart  14951  sadadd2lem2  16157  isnirred  19942  isreg2  22528  kqcldsat  22884  trufil  23061  itg2cnlem2  24927  issqf  26285  eupth2lem3lem4  28595  pjnorm2  30089  atdmd  30760  atmd2  30762  dfrdg4  34253  dalawlem13  37897  sticksstones1  40102  infordmin  41139