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  2369  cbvexd  2438  cbvrexdva  3244  raleq  3317  cbvrexdva2  3338  rexeqf  3343  cbvexeqsetf  3466  sbcne12  4373  ordsucuniel  7835  rankr1a  9848  ltaddsub  11790  leaddsub  11792  supxrbnd1  13451  supxrbnd2  13452  ioo0  13501  ico0  13522  ioc0  13523  icc0  13524  fllt  13946  rabssnn0fi  14129  elcls  23391  ltsrec  28187  rusgrnumwwlks  30566  chrelat3  32973  bj-equsexvwd  37675  wl-sb8eft  38483  wl-sb8et  38485  wl-issetft  38514  infxrbnd2  46379  nprmmul1  48608  oddprmne2  48812  nnolog2flm1  49701