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  4412  ordsucuniel  7809  rankr1a  9828  ltaddsub  11685  leaddsub  11687  supxrbnd1  13297  supxrbnd2  13298  ioo0  13346  ico0  13367  ioc0  13368  icc0  13369  fllt  13768  rabssnn0fi  13948  elcls  22569  sltrec  27311  rusgrnumwwlks  29218  chrelat3  31612  bj-equsexvwd  35648  wl-sb8et  36407  wl-issetft  36433  infxrbnd2  44066  oddprmne2  46370  nnolog2flm1  47230