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  2407  cbvrexdva  3219  raleq  3298  rexeqbidvvOLD  3312  cbvrexdva2  3324  rexeqf  3332  cbvexeqsetf  3465  sbcne12  4381  ordsucuniel  7802  rankr1a  9796  ltaddsub  11659  leaddsub  11661  supxrbnd1  13288  supxrbnd2  13289  ioo0  13338  ico0  13359  ioc0  13360  icc0  13361  fllt  13775  rabssnn0fi  13958  elcls  22967  sltrec  27739  rusgrnumwwlks  29911  chrelat3  32307  bj-equsexvwd  36776  wl-sb8eft  37546  wl-sb8et  37548  wl-issetft  37577  infxrbnd2  45372  oddprmne2  47720  nnolog2flm1  48583