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  375  had0  1603  cbvexdvaw  2040  cbvexdw  2333  cbvexd  2405  cbvrexdva  3235  raleq  3320  rexeqbidvvOLD  3330  cbvrexdva2  3343  rexeqf  3348  issetft  3486  sbcne12  4411  ordsucuniel  7814  rankr1a  9833  ltaddsub  11692  leaddsub  11694  supxrbnd1  13304  supxrbnd2  13305  ioo0  13353  ico0  13374  ioc0  13375  icc0  13376  fllt  13775  rabssnn0fi  13955  elcls  22797  sltrec  27558  rusgrnumwwlks  29495  chrelat3  31891  bj-equsexvwd  35962  wl-sb8et  36721  wl-issetft  36747  infxrbnd2  44377  oddprmne2  46681  nnolog2flm1  47363