Theorem con1bid 344

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

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

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 197

This theorem is referenced by:  pm5.18  370  necon1bbid  2972  r19.9rzv  4210  onmindif  5977  iotanul  6028  ondif2  7754  cnpart  14200  sadadd2lem2  15395  isnirred  18921  isreg2  21404  kqcldsat  21759  trufil  21936  itg2cnlem2  23749  issqf  25083  eupth2lem3lem4  27405  pjnorm2  28917  atdmd  29588  atmd2  29590  dfrdg4  32386  dalawlem13  35691