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  1606  cbvexdvaw  2041  cbvexdw  2343  cbvexd  2412  cbvrexdva  3218  raleq  3292  cbvrexdva2  3314  rexeqf  3319  cbvexeqsetf  3444  sbcne12  4355  ordsucuniel  7775  rankr1a  9760  ltaddsub  11624  leaddsub  11626  supxrbnd1  13273  supxrbnd2  13274  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  fllt  13765  rabssnn0fi  13948  elcls  23038  ltsrec  27793  rusgrnumwwlks  30045  chrelat3  32442  bj-equsexvwd  37070  wl-sb8eft  37876  wl-sb8et  37878  wl-issetft  37907  infxrbnd2  45798  nprmmul1  47987  oddprmne2  48191  nnolog2flm1  49066