Theorem con4bid 319

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

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

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 209

This theorem is referenced by:  notbid  320  notbi  321  2falsed  378  had0  1618  cbvexdvaw  2053  cbvexdw  2364  cbvexd  2433  cbvrexdva  3237  raleq  3311  cbvrexdva2  3333  rexeqf  3338  cbvexeqsetf  3463  sbcne12  4363  ordsucuniel  7793  rankr1a  9784  ltaddsub  11651  leaddsub  11653  supxrbnd1  13314  supxrbnd2  13315  ioo0  13364  ico0  13385  ioc0  13386  icc0  13387  fllt  13806  rabssnn0fi  13989  elcls  23106  ltsrec  27864  rusgrnumwwlks  30116  chrelat3  32513  bj-equsexvwd  37196  wl-sb8eft  38002  wl-sb8et  38004  wl-issetft  38033  infxrbnd2  45892  nprmmul1  48081  oddprmne2  48285  nnolog2flm1  49160