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  2964  r19.9rzv  4451  rexsng  4628  onmindif  6401  iotanul  6462  ondif2  8420  cnpart  15147  sadadd2lem2  16361  isnirred  20305  isreg2  23262  kqcldsat  23618  trufil  23795  itg2cnlem2  25661  issqf  27044  eupth2lem3lem4  30175  pjnorm2  31671  atdmd  32342  atmd2  32344  dfrdg4  35935  dalawlem13  39872  sticksstones1  42129  aks6d1c6lem4  42156  orddif0suc  43251  infordmin  43515