Theorem con4bid 320

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 251	. . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1	biimpd 232	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
5	3, 4	impcon4bid 230	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  notbi  322  2falsed  379  had0OLD  1636  cbvexdvaw  2072  cbvexdw  2373  cbvexd  2442  cbvrexdva  3248  raleq  3322  cbvrexdva2  3343  rexeqf  3348  cbvexeqsetf  3472  sbcne12  4380  ordsucuniel  7826  rankr1a  9815  ltaddsub  11705  leaddsub  11707  supxrbnd1  13365  supxrbnd2  13366  ioo0  13415  ico0  13436  ioc0  13437  icc0  13438  fllt  13859  rabssnn0fi  14042  elcls  23282  ltsrec  28047  rusgrnumwwlks  30395  chrelat3  32796  bj-equsexvwd  37457  wl-sb8eft  38265  wl-sb8et  38267  wl-issetft  38296  infxrbnd2  46144  nprmmul1  48336  oddprmne2  48540  nnolog2flm1  49429