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  3218  raleq  3296  rexeqbidvvOLD  3310  cbvrexdva2  3322  rexeqf  3330  cbvexeqsetf  3462  sbcne12  4378  ordsucuniel  7799  rankr1a  9789  ltaddsub  11652  leaddsub  11654  supxrbnd1  13281  supxrbnd2  13282  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  fllt  13768  rabssnn0fi  13951  elcls  22960  sltrec  27732  rusgrnumwwlks  29904  chrelat3  32300  bj-equsexvwd  36769  wl-sb8eft  37539  wl-sb8et  37541  wl-issetft  37570  infxrbnd2  45365  oddprmne2  47716  nnolog2flm1  48579