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  2967  r19.9rzv  4449  rexsng  4628  onmindif  6406  iotanul  6467  ondif2  8423  cnpart  15153  sadadd2lem2  16367  isnirred  20344  isreg2  23298  kqcldsat  23654  trufil  23831  itg2cnlem2  25696  issqf  27079  eupth2lem3lem4  30218  pjnorm2  31714  atdmd  32385  atmd2  32387  dfrdg4  36002  dalawlem13  39988  sticksstones1  42245  aks6d1c6lem4  42272  orddif0suc  43366  infordmin  43630