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

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

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 196

This theorem is referenced by:  pm5.18  370  necon1bbid  2821  r19.9rzv  4017  onmindif  5732  ondif2  7469  cnpart  13828  sadadd2lem2  15010  isnirred  18523  isreg2  20991  kqcldsat  21346  trufil  21524  itg2cnlem2  23335  issqf  24662  eupath2lem3  26506  pjnorm2  27970  atdmd  28641  atmd2  28643  dfrdg4  31228  dalawlem13  34187  eupth2lem3lem4  41399