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  1635  cbvexdvaw  2071  cbvexdw  2368  cbvexd  2437  cbvrexdva  3243  raleq  3316  cbvrexdva2  3337  rexeqf  3342  cbvexeqsetf  3465  sbcne12  4372  ordsucuniel  7839  rankr1a  9855  ltaddsub  11797  leaddsub  11799  supxrbnd1  13458  supxrbnd2  13459  ioo0  13508  ico0  13529  ioc0  13530  icc0  13531  fllt  13953  rabssnn0fi  14136  elcls  23400  ltsrec  28196  rusgrnumwwlks  30575  chrelat3  32982  bj-equsexvwd  37799  wl-sb8eft  38620  wl-sb8et  38622  wl-issetft  38651  infxrbnd2  46516  nprmmul1  48745  oddprmne2  48949  nnolog2flm1  49838