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  2038  cbvexdw  2345  cbvexd  2416  cbvrexdva  3246  raleq  3331  rexeqbidvvOLD  3345  cbvrexdva2  3357  rexeqf  3362  cbvexeqsetf  3503  sbcne12  4438  ordsucuniel  7860  rankr1a  9905  ltaddsub  11764  leaddsub  11766  supxrbnd1  13383  supxrbnd2  13384  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  fllt  13857  rabssnn0fi  14037  elcls  23102  sltrec  27883  rusgrnumwwlks  30007  chrelat3  32403  bj-equsexvwd  36747  wl-sb8eft  37505  wl-sb8et  37507  wl-issetft  37536  infxrbnd2  45284  oddprmne2  47589  nnolog2flm1  48324