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  2967  r19.9rzv  4447  rexsng  4626  onmindif  6400  iotanul  6461  ondif2  8417  cnpart  15147  sadadd2lem2  16361  isnirred  20338  isreg2  23292  kqcldsat  23648  trufil  23825  itg2cnlem2  25690  issqf  27073  eupth2lem3lem4  30211  pjnorm2  31707  atdmd  32378  atmd2  32380  dfrdg4  35995  dalawlem13  39981  sticksstones1  42238  aks6d1c6lem4  42265  orddif0suc  43360  infordmin  43624