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  2341  cbvexd  2413  cbvrexdva  3240  raleq  3323  rexeqbidvvOLD  3337  cbvrexdva2  3349  rexeqf  3354  cbvexeqsetf  3495  sbcne12  4415  ordsucuniel  7844  rankr1a  9876  ltaddsub  11737  leaddsub  11739  supxrbnd1  13363  supxrbnd2  13364  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  fllt  13846  rabssnn0fi  14027  elcls  23081  sltrec  27865  rusgrnumwwlks  29994  chrelat3  32390  bj-equsexvwd  36782  wl-sb8eft  37552  wl-sb8et  37554  wl-issetft  37583  infxrbnd2  45380  oddprmne2  47702  nnolog2flm1  48511