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  3286  rexeqbidvvOLD  3300  cbvrexdva2  3312  rexeqf  3319  cbvexeqsetf  3451  sbcne12  4366  ordsucuniel  7757  rankr1a  9732  ltaddsub  11594  leaddsub  11596  supxrbnd1  13223  supxrbnd2  13224  ioo0  13273  ico0  13294  ioc0  13295  icc0  13296  fllt  13710  rabssnn0fi  13893  elcls  22958  sltrec  27732  rusgrnumwwlks  29919  chrelat3  32315  bj-equsexvwd  36759  wl-sb8eft  37529  wl-sb8et  37531  wl-issetft  37560  infxrbnd2  45352  oddprmne2  47703  nnolog2flm1  48579