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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  notbid  321  notbi  322  2falsed  379  had0  1634  cbvexdvaw  2069  cbvexdw  2371  cbvexd  2440  cbvrexdva  3246  raleq  3320  cbvrexdva2  3341  rexeqf  3346  cbvexeqsetf  3470  sbcne12  4380  ordsucuniel  7816  rankr1a  9804  ltaddsub  11683  leaddsub  11685  supxrbnd1  13342  supxrbnd2  13343  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  fllt  13835  rabssnn0fi  14018  elcls  23230  ltsrec  27994  rusgrnumwwlks  30326  chrelat3  32723  bj-equsexvwd  37398  wl-sb8eft  38206  wl-sb8et  38208  wl-issetft  38237  infxrbnd2  46084  nprmmul1  48276  oddprmne2  48480  nnolog2flm1  49370