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  1605  cbvexdvaw  2040  cbvexdw  2339  cbvexd  2408  cbvrexdva  3213  raleq  3289  rexeqbidvvOLD  3303  cbvrexdva2  3315  rexeqf  3322  cbvexeqsetf  3451  sbcne12  4362  ordsucuniel  7754  rankr1a  9729  ltaddsub  11591  leaddsub  11593  supxrbnd1  13220  supxrbnd2  13221  ioo0  13270  ico0  13291  ioc0  13292  icc0  13293  fllt  13710  rabssnn0fi  13893  elcls  22988  sltrec  27762  rusgrnumwwlks  29955  chrelat3  32351  bj-equsexvwd  36825  wl-sb8eft  37595  wl-sb8et  37597  wl-issetft  37626  infxrbnd2  45477  oddprmne2  47825  nnolog2flm1  48701