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  1598  cbvexdvaw  2035  cbvexdw  2330  cbvexd  2402  cbvrexdva  3228  raleq  3312  rexeqbidvvOLD  3322  cbvrexdva2  3333  rexeqf  3338  issetft  3477  sbcne12  4417  ordsucuniel  7833  rankr1a  9879  ltaddsub  11738  leaddsub  11740  supxrbnd1  13354  supxrbnd2  13355  ioo0  13403  ico0  13424  ioc0  13425  icc0  13426  fllt  13826  rabssnn0fi  14006  elcls  23068  sltrec  27850  rusgrnumwwlks  29908  chrelat3  32304  bj-equsexvwd  36486  wl-sb8eft  37246  wl-sb8et  37248  wl-issetft  37277  infxrbnd2  44984  oddprmne2  47287  nnolog2flm1  47978