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  1631  cbvexdvaw  2066  cbvexdw  2377  cbvexd  2446  cbvrexdva  3252  raleq  3326  cbvrexdva2  3348  rexeqf  3353  cbvexeqsetf  3478  sbcne12  4386  ordsucuniel  7819  rankr1a  9807  ltaddsub  11687  leaddsub  11689  supxrbnd1  13346  supxrbnd2  13347  ioo0  13396  ico0  13417  ioc0  13418  icc0  13419  fllt  13838  rabssnn0fi  14021  elcls  23198  ltsrec  27959  rusgrnumwwlks  30266  chrelat3  32663  bj-equsexvwd  37286  wl-sb8eft  38093  wl-sb8et  38095  wl-issetft  38124  infxrbnd2  45975  nprmmul1  48164  oddprmne2  48368  nnolog2flm1  49254