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  1607  cbvexdvaw  2043  cbvexdw  2338  cbvexd  2408  rexeqbidvv  3330  vtoclgft  3482  sbcne12  4343  ordsucuniel  7646  rankr1a  9525  ltaddsub  11379  leaddsub  11381  supxrbnd1  12984  supxrbnd2  12985  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  fllt  13454  rabssnn0fi  13634  elcls  22132  rusgrnumwwlks  28240  chrelat3  30634  sltrec  33941  bj-equsexvwd  34890  wl-sb8et  35635  infxrbnd2  42798  oddprmne2  45055  nnolog2flm1  45824