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  3295  rexeqbidvvOLD  3309  cbvrexdva2  3321  rexeqf  3328  cbvexeqsetf  3457  sbcne12  4369  ordsucuniel  7776  rankr1a  9760  ltaddsub  11623  leaddsub  11625  supxrbnd1  13248  supxrbnd2  13249  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  fllt  13738  rabssnn0fi  13921  elcls  23029  ltsrec  27809  rusgrnumwwlks  30062  chrelat3  32459  bj-equsexvwd  37016  wl-sb8eft  37806  wl-sb8et  37808  wl-issetft  37837  infxrbnd2  45727  oddprmne2  48075  nnolog2flm1  48950