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

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

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 206

This theorem is referenced by:  notbid  318  notbi  319  2falsed  377  had0  1606  cbvexdvaw  2043  cbvexdw  2336  cbvexd  2408  cbvrexdva  3238  raleq  3323  rexeqbidvvOLD  3333  cbvrexdva2  3346  rexeqf  3351  vtoclgft  3541  sbcne12  4413  ordsucuniel  7812  rankr1a  9831  ltaddsub  11688  leaddsub  11690  supxrbnd1  13300  supxrbnd2  13301  ioo0  13349  ico0  13370  ioc0  13371  icc0  13372  fllt  13771  rabssnn0fi  13951  elcls  22577  sltrec  27321  rusgrnumwwlks  29228  chrelat3  31624  bj-equsexvwd  35659  wl-sb8et  36418  wl-issetft  36444  infxrbnd2  44079  oddprmne2  46383  nnolog2flm1  47276