Theorem con4bid 318

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

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

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 208

This theorem is referenced by:  notbid  319  notbi  320  had0  1590  cbvexd  2387  cbvrexdva2OLD  3411  vtoclgft  3499  sbcne12  4290  ordsucuniel  7402  rankr1a  9118  ltaddsub  10968  leaddsub  10970  supxrbnd1  12568  supxrbnd2  12569  ioo0  12617  ico0  12638  ioc0  12639  icc0  12640  fllt  13030  rabssnn0fi  13208  elcls  21369  rusgrnumwwlks  27439  chrelat3  29835  sltrec  32889  wl-sb8et  34341  infxrbnd2  41199  oddprmne2  43384  nnolog2flm1  44153