Theorem con4bid 318

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

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

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 208

This theorem is referenced by:  notbid  319  notbi  320  2falsed  377  had0  1611  cbvexdvaw  2046  cbvexdw  2347  cbvexd  2416  cbvrexdva  3220  raleq  3294  cbvrexdva2  3316  rexeqf  3321  cbvexeqsetf  3446  sbcne12  4343  ordsucuniel  7764  rankr1a  9751  ltaddsub  11615  leaddsub  11617  supxrbnd1  13264  supxrbnd2  13265  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  fllt  13756  rabssnn0fi  13939  elcls  23056  ltsrec  27811  rusgrnumwwlks  30063  chrelat3  32460  bj-equsexvwd  37116  wl-sb8eft  37922  wl-sb8et  37924  wl-issetft  37953  infxrbnd2  45813  nprmmul1  48002  oddprmne2  48206  nnolog2flm1  49081