Theorem con1bid 359

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

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

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 210

This theorem is referenced by:  pm5.18  386  necon1bbid  2990  r19.9rzv  4396  onmindif  6263  iotanul  6318  ondif2  8143  cnpart  14660  sadadd2lem2  15862  isnirred  19534  isreg2  22090  kqcldsat  22446  trufil  22623  itg2cnlem2  24475  issqf  25833  eupth2lem3lem4  28128  pjnorm2  29622  atdmd  30293  atmd2  30295  dfrdg4  33836  dalawlem13  37493  infordmin  40648