Theorem con1bid 355

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

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

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 207

This theorem is referenced by:  pm5.18  381  necon1bbid  2969  r19.9rzv  4456  rexsng  4631  onmindif  6409  iotanul  6470  ondif2  8427  cnpart  15161  sadadd2lem2  16375  isnirred  20354  isreg2  23319  kqcldsat  23675  trufil  23852  itg2cnlem2  25717  issqf  27100  eupth2lem3lem4  30255  pjnorm2  31751  atdmd  32422  atmd2  32424  dfrdg4  36094  dalawlem13  40082  sticksstones1  42339  aks6d1c6lem4  42366  orddif0suc  43452  infordmin  43715