Theorem con1bid 358

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.18  384  necon1bbid  2996  r19.9rzv  4464  rexsng  4640  onmindif  6456  iotanul  6517  ondif2  8492  cnpart  15329  sadadd2lem2  16544  isnirred  20562  isreg2  23603  kqcldsat  23960  trufil  24137  itg2cnlem2  25991  issqf  27370  eupth2lem3lem4  30697  pjnorm2  32194  atdmd  32865  atmd2  32867  dfrdg4  36517  nmulle  36784  qdiffALT  38067  dalawlem13  40743  sticksstones1  42999  aks6d1c6lem4  43026  orddif0suc  44096  infordmin  44359  prmringnzring  49239