Theorem con4bid 320

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 251	. . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1	biimpd 232	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
5	3, 4	impcon4bid 230	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  notbi  322  2falsed  379  had0OLD  1636  cbvexdvaw  2072  cbvexdw  2368  cbvexd  2437  cbvrexdva  3243  raleq  3316  cbvrexdva2  3337  rexeqf  3342  cbvexeqsetf  3465  sbcne12  4373  ordsucuniel  7821  rankr1a  9819  ltaddsub  11713  leaddsub  11715  supxrbnd1  13374  supxrbnd2  13375  ioo0  13424  ico0  13445  ioc0  13446  icc0  13447  fllt  13868  rabssnn0fi  14051  elcls  23299  ltsrec  28067  rusgrnumwwlks  30446  chrelat3  32853  bj-equsexvwd  37507  wl-sb8eft  38315  wl-sb8et  38317  wl-issetft  38346  infxrbnd2  46199  nprmmul1  48428  oddprmne2  48632  nnolog2flm1  49521