Theorem con1bid 357

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 225	. . 3 ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓))
3	2	con2bid 356	. 2 ⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒))
4	3	bicomd 225	1 ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pm5.18  383  necon1bbid  2998  r19.9rzv  4461  rexsng  4637  onmindif  6442  iotanul  6503  ondif2  8473  cnpart  15269  sadadd2lem2  16486  isnirred  20471  isreg2  23439  kqcldsat  23795  trufil  23972  itg2cnlem2  25826  issqf  27202  eupth2lem3lem4  30435  pjnorm2  31932  atdmd  32603  atmd2  32605  dfrdg4  36306  qdiffALT  37825  dalawlem13  40512  sticksstones1  42768  aks6d1c6lem4  42795  orddif0suc  43850  infordmin  44113