Theorem con4bid 320

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

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

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 210

This theorem is referenced by:  notbid  321  notbi  322  2falsed  380  had0  1610  cbvexdvaw  2051  cbvexdw  2342  cbvexd  2409  rexeqbidvv  3308  vtoclgft  3460  sbcne12  4312  ordsucuniel  7570  rankr1a  9350  ltaddsub  11204  leaddsub  11206  supxrbnd1  12809  supxrbnd2  12810  ioo0  12858  ico0  12879  ioc0  12880  icc0  12881  fllt  13279  rabssnn0fi  13457  elcls  21836  rusgrnumwwlks  27924  chrelat3  30318  sltrec  33669  bj-equsexvwd  34618  wl-sb8et  35363  infxrbnd2  42486  oddprmne2  44748  nnolog2flm1  45517