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  2972  r19.9rzv  4459  rexsng  4634  onmindif  6412  iotanul  6473  ondif2  8431  cnpart  15167  sadadd2lem2  16381  isnirred  20360  isreg2  23325  kqcldsat  23681  trufil  23858  itg2cnlem2  25723  issqf  27106  eupth2lem3lem4  30310  pjnorm2  31806  atdmd  32477  atmd2  32479  dfrdg4  36147  dalawlem13  40211  sticksstones1  42468  aks6d1c6lem4  42495  orddif0suc  43577  infordmin  43840