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  4465  rexsng  4641  onmindif  6455  iotanul  6516  ondif2  8485  cnpart  15298  sadadd2lem2  16514  isnirred  20509  isreg2  23545  kqcldsat  23901  trufil  24078  itg2cnlem2  25932  issqf  27311  eupth2lem3lem4  30593  pjnorm2  32090  atdmd  32761  atmd2  32763  dfrdg4  36451  nmulle  36717  qdiffALT  38000  dalawlem13  40685  sticksstones1  42941  aks6d1c6lem4  42968  orddif0suc  44023  infordmin  44286  prmringnzring  49130