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  2998  r19.9rzv  4464  rexsng  4637  onmindif  6472  iotanul  6534  ondif2  8535  cnpart  15433  sadadd2lem2  16646  isnirred  20677  isreg2  23722  kqcldsat  24079  trufil  24256  itg2cnlem2  26110  issqf  27490  eupth2lem3lem4  30859  pjnorm2  32356  atdmd  33027  atmd2  33029  dfrdg4  36892  nmulle  37143  qdiffALT  38440  dalawlem13  41131  sticksstones1  43387  aks6d1c6lem4  43414  orddif0suc  44460  infordmin  44723  prmringnzring  49637