Theorem con4bid 306

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 237	. . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 113	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1	biimpd 218	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
5	3, 4	impcon4bid 216	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  notbid  307  notbi  308  had0  1534  cbvexdva  2271  sbcne12  3938  ordsucuniel  6916  rankr1a  8582  ltaddsub  10381  leaddsub  10383  supxrbnd1  12023  supxrbnd2  12024  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  fllt  12469  rabssnn0fi  12647  elcls  20687  rusgranumwlks  26483  chrelat3  28614  wl-sb8et  32513  infxrbnd2  38526  oddprmne2  40162  rusgrnumwwlks  41177  nnolog2flm1  42182