Theorem con4bid 317

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  318  notbi  319  2falsed  377  had0  1606  cbvexdvaw  2043  cbvexdw  2337  cbvexd  2409  rexeqbidvv  3340  vtoclgft  3493  sbcne12  4347  ordsucuniel  7680  rankr1a  9603  ltaddsub  11458  leaddsub  11460  supxrbnd1  13064  supxrbnd2  13065  ioo0  13113  ico0  13134  ioc0  13135  icc0  13136  fllt  13535  rabssnn0fi  13715  elcls  22233  rusgrnumwwlks  28348  chrelat3  30742  sltrec  34023  bj-equsexvwd  34972  wl-sb8et  35717  infxrbnd2  42915  oddprmne2  45178  nnolog2flm1  45947