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  3210  raleq  3287  rexeqbidvvOLD  3301  cbvrexdva2  3313  rexeqf  3321  cbvexeqsetf  3453  sbcne12  4368  ordsucuniel  7763  rankr1a  9751  ltaddsub  11613  leaddsub  11615  supxrbnd1  13242  supxrbnd2  13243  ioo0  13292  ico0  13313  ioc0  13314  icc0  13315  fllt  13729  rabssnn0fi  13912  elcls  22977  sltrec  27751  rusgrnumwwlks  29938  chrelat3  32334  bj-equsexvwd  36774  wl-sb8eft  37544  wl-sb8et  37546  wl-issetft  37575  infxrbnd2  45368  oddprmne2  47719  nnolog2flm1  48595