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  2965  r19.9rzv  4466  rexsng  4643  onmindif  6429  iotanul  6492  ondif2  8469  cnpart  15213  sadadd2lem2  16427  isnirred  20336  isreg2  23271  kqcldsat  23627  trufil  23804  itg2cnlem2  25670  issqf  27053  eupth2lem3lem4  30167  pjnorm2  31663  atdmd  32334  atmd2  32336  dfrdg4  35946  dalawlem13  39884  sticksstones1  42141  aks6d1c6lem4  42168  orddif0suc  43264  infordmin  43528