Theorem con4bid 317

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 248	. . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 115	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1	biimpd 229	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
5	3, 4	impcon4bid 227	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

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

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 207

This theorem is referenced by:  notbid  318  notbi  319  2falsed  376  had0  1606  cbvexdvaw  2041  cbvexdw  2344  cbvexd  2413  cbvrexdva  3219  raleq  3293  cbvrexdva2  3315  rexeqf  3320  cbvexeqsetf  3445  sbcne12  4356  ordsucuniel  7769  rankr1a  9754  ltaddsub  11618  leaddsub  11620  supxrbnd1  13267  supxrbnd2  13268  ioo0  13317  ico0  13338  ioc0  13339  icc0  13340  fllt  13759  rabssnn0fi  13942  elcls  23051  ltsrec  27810  rusgrnumwwlks  30063  chrelat3  32460  bj-equsexvwd  37089  wl-sb8eft  37893  wl-sb8et  37895  wl-issetft  37924  infxrbnd2  45819  nprmmul1  48002  oddprmne2  48206  nnolog2flm1  49081