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  4480  rexsng  4657  onmindif  6451  iotanul  6514  ondif2  8519  cnpart  15264  sadadd2lem2  16474  isnirred  20385  isreg2  23320  kqcldsat  23676  trufil  23853  itg2cnlem2  25720  issqf  27103  eupth2lem3lem4  30217  pjnorm2  31713  atdmd  32384  atmd2  32386  dfrdg4  35974  dalawlem13  39907  sticksstones1  42164  aks6d1c6lem4  42191  orddif0suc  43259  infordmin  43523