Theorem con4bid 319

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

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

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 209

This theorem is referenced by:  notbid  320  notbi  321  2falsed  379  had0  1601  cbvexdvaw  2042  cbvexdw  2355  cbvexd  2425  cbvrexdva2OLD  3458  vtoclgft  3553  sbcne12  4363  ordsucuniel  7538  rankr1a  9264  ltaddsub  11113  leaddsub  11115  supxrbnd1  12713  supxrbnd2  12714  ioo0  12762  ico0  12783  ioc0  12784  icc0  12785  fllt  13175  rabssnn0fi  13353  elcls  21680  rusgrnumwwlks  27752  chrelat3  30147  sltrec  33278  wl-sb8et  34788  infxrbnd2  41635  oddprmne2  43879  nnolog2flm1  44649