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  2994  r19.9rzv  4461  rexsng  4637  onmindif  6447  iotanul  6508  ondif2  8489  cnpart  15360  sadadd2lem2  16573  isnirred  20597  isreg2  23642  kqcldsat  23999  trufil  24176  itg2cnlem2  26030  issqf  27412  eupth2lem3lem4  30751  pjnorm2  32248  atdmd  32919  atmd2  32921  dfrdg4  36631  nmulle  36882  qdiffALT  38163  dalawlem13  40854  sticksstones1  43110  aks6d1c6lem4  43137  orddif0suc  44207  infordmin  44470  prmringnzring  49350