Theorem con4bid 319

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

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

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 209

This theorem is referenced by:  notbid  320  notbi  321  2falsed  378  had0  1624  cbvexdvaw  2059  cbvexdw  2370  cbvexd  2439  cbvrexdva  3243  raleq  3317  cbvrexdva2  3339  rexeqf  3344  cbvexeqsetf  3469  sbcne12  4369  ordsucuniel  7804  rankr1a  9794  ltaddsub  11661  leaddsub  11663  supxrbnd1  13324  supxrbnd2  13325  ioo0  13374  ico0  13395  ioc0  13396  icc0  13397  fllt  13816  rabssnn0fi  13999  elcls  23133  ltsrec  27894  rusgrnumwwlks  30177  chrelat3  32574  bj-equsexvwd  37248  wl-sb8eft  38054  wl-sb8et  38056  wl-issetft  38085  infxrbnd2  45944  nprmmul1  48133  oddprmne2  48337  nnolog2flm1  49212