Theorem con4bid 317

Description: A contraposition deduction. (Contributed by NM, 21-May-1994.)

Hypothesis

Ref	Expression
con4bid.1	⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Assertion

Ref	Expression
con4bid	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem con4bid

Step	Hyp	Ref	Expression
1		con4bid.1	. . . 4 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
2	1	biimprd 248	. . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 115	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1	biimpd 229	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
5	3, 4	impcon4bid 227	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:  notbid  318  notbi  319  2falsed  376  had0  1604  cbvexdvaw  2039  cbvexdw  2337  cbvexd  2406  cbvrexdva  3216  raleq  3293  rexeqbidvvOLD  3307  cbvrexdva2  3319  rexeqf  3327  cbvexeqsetf  3459  sbcne12  4374  ordsucuniel  7779  rankr1a  9765  ltaddsub  11628  leaddsub  11630  supxrbnd1  13257  supxrbnd2  13258  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  fllt  13744  rabssnn0fi  13927  elcls  22936  sltrec  27708  rusgrnumwwlks  29877  chrelat3  32273  bj-equsexvwd  36742  wl-sb8eft  37512  wl-sb8et  37514  wl-issetft  37543  infxrbnd2  45338  oddprmne2  47689  nnolog2flm1  48552