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 ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓))

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

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 210

This theorem is referenced by:  pm5.18  384  necon1bbid  3003  r19.9rzv  4469  rexsng  4645  onmindif  6456  iotanul  6517  ondif2  8487  cnpart  15291  sadadd2lem2  16508  isnirred  20502  isreg2  23503  kqcldsat  23859  trufil  24036  itg2cnlem2  25890  issqf  27266  eupth2lem3lem4  30523  pjnorm2  32020  atdmd  32691  atmd2  32693  dfrdg4  36376  qdiffALT  37895  dalawlem13  40582  sticksstones1  42838  aks6d1c6lem4  42865  orddif0suc  43922  infordmin  44185  prmringnzring  49026