Theorem sylbird 169

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbird.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
sylbird.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbird	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 157	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  drex1  1771  eqreu  2880  onsucsssucr  4433  ordsucunielexmid  4454  ovi3  5915  tfrlem9  6224  dom2lem  6674  distrlem4prl  7416  distrlem4pru  7417  recexprlemm  7456  caucvgprlem1  7511  caucvgprprlemexb  7539  aptisr  7611  map2psrprg  7637  renegcl  8047  addid0  8159  remulext2  8386  mulext1  8398  apmul1  8572  nnge1  8767  0mnnnnn0  9033  nn0lt2  9156  zneo  9176  uzind2  9187  fzind  9190  nn0ind-raph  9192  ledivge1le  9543  elfzmlbp  9940  difelfznle  9943  elfzodifsumelfzo  10009  ssfzo12  10032  flqeqceilz  10122  addmodlteq  10202  uzsinds  10246  facdiv  10516  facwordi  10518  bcpasc  10544  addcn2  11111  mulcn2  11113  climrecvg1n  11149  odd2np1  11606  oddge22np1  11614  gcdaddm  11708  algcvgblem  11766  cncongr1  11820  metss2lem  12705