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  1605  cbvexdvaw  2040  cbvexdw  2341  cbvexd  2410  cbvrexdva  3215  raleq  3291  rexeqbidvvOLD  3305  cbvrexdva2  3317  rexeqf  3324  cbvexeqsetf  3453  sbcne12  4365  ordsucuniel  7764  rankr1a  9746  ltaddsub  11609  leaddsub  11611  supxrbnd1  13234  supxrbnd2  13235  ioo0  13284  ico0  13305  ioc0  13306  icc0  13307  fllt  13724  rabssnn0fi  13907  elcls  23015  sltrec  27789  rusgrnumwwlks  29999  chrelat3  32395  bj-equsexvwd  36925  wl-sb8eft  37695  wl-sb8et  37697  wl-issetft  37726  infxrbnd2  45555  oddprmne2  47903  nnolog2flm1  48778