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  2038  cbvexdw  2340  cbvexd  2412  cbvrexdva  3223  raleq  3302  rexeqbidvvOLD  3316  cbvrexdva2  3328  rexeqf  3333  cbvexeqsetf  3474  sbcne12  4390  ordsucuniel  7818  rankr1a  9850  ltaddsub  11711  leaddsub  11713  supxrbnd1  13337  supxrbnd2  13338  ioo0  13387  ico0  13408  ioc0  13409  icc0  13410  fllt  13823  rabssnn0fi  14004  elcls  23011  sltrec  27784  rusgrnumwwlks  29956  chrelat3  32352  bj-equsexvwd  36799  wl-sb8eft  37569  wl-sb8et  37571  wl-issetft  37600  infxrbnd2  45396  oddprmne2  47729  nnolog2flm1  48570