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  2074  cbvexdw  2372  cbvexd  2440  cbvrexdva  3247  raleq  3320  cbvrexdva2  3341  rexeqf  3346  cbvexeqsetf  3469  sbcne12  4376  ordsucuniel  7869  rankr1a  9885  ltaddsub  11830  leaddsub  11832  supxrbnd1  13491  supxrbnd2  13492  ioo0  13541  ico0  13562  ioc0  13563  icc0  13564  fllt  13986  rabssnn0fi  14169  elcls  23446  ltsrec  28244  rusgrnumwwlks  30623  chrelat3  33030  bj-equsexvwd  37890  wl-sb8eft  38751  wl-sb8et  38753  wl-issetft  38782  infxrbnd2  46653  nprmmul1  48882  oddprmne2  49086  nnolog2flm1  50033