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

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

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 207

This theorem is referenced by:  notbid  318  notbi  319  2falsed  376  had0  1601  cbvexdvaw  2036  cbvexdw  2340  cbvexd  2411  cbvrexdva  3238  raleq  3321  rexeqbidvvOLD  3335  cbvrexdva2  3347  rexeqf  3352  cbvexeqsetf  3493  sbcne12  4421  ordsucuniel  7844  rankr1a  9874  ltaddsub  11735  leaddsub  11737  supxrbnd1  13360  supxrbnd2  13361  ioo0  13409  ico0  13430  ioc0  13431  icc0  13432  fllt  13843  rabssnn0fi  14024  elcls  23097  sltrec  27880  rusgrnumwwlks  30004  chrelat3  32400  bj-equsexvwd  36764  wl-sb8eft  37532  wl-sb8et  37534  wl-issetft  37563  infxrbnd2  45319  oddprmne2  47640  nnolog2flm1  48440