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  2343  cbvexd  2412  cbvrexdva  3217  raleq  3293  rexeqbidvvOLD  3307  cbvrexdva2  3319  rexeqf  3326  cbvexeqsetf  3455  sbcne12  4367  ordsucuniel  7766  rankr1a  9748  ltaddsub  11611  leaddsub  11613  supxrbnd1  13236  supxrbnd2  13237  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  fllt  13726  rabssnn0fi  13909  elcls  23017  ltsrec  27797  rusgrnumwwlks  30050  chrelat3  32446  bj-equsexvwd  36982  wl-sb8eft  37756  wl-sb8et  37758  wl-issetft  37787  infxrbnd2  45613  oddprmne2  47961  nnolog2flm1  48836