Theorem con4bid 316

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

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

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 206

This theorem is referenced by:  notbid  317  notbi  318  2falsed  376  had0  1605  cbvexdvaw  2042  cbvexdw  2335  cbvexd  2406  cbvrexdva  3236  raleq  3321  rexeqbidvvOLD  3331  cbvrexdva2  3344  rexeqf  3349  vtoclgft  3537  sbcne12  4408  ordsucuniel  7795  rankr1a  9813  ltaddsub  11670  leaddsub  11672  supxrbnd1  13282  supxrbnd2  13283  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  fllt  13753  rabssnn0fi  13933  elcls  22506  sltrec  27247  rusgrnumwwlks  29093  chrelat3  31487  bj-equsexvwd  35463  wl-sb8et  36222  wl-issetft  36248  infxrbnd2  43852  oddprmne2  46155  nnolog2flm1  46924