Theorem sylbird 170

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 158	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  drex1  1798  eqreu  2931  onsucsssucr  4510  ordsucunielexmid  4532  ovi3  6013  tfrlem9  6322  dom2lem  6774  distrlem4prl  7585  distrlem4pru  7586  recexprlemm  7625  caucvgprlem1  7680  caucvgprprlemexb  7708  aptisr  7780  map2psrprg  7806  renegcl  8220  addid0  8332  remulext2  8559  mulext1  8571  apmul1  8747  nnge1  8944  0mnnnnn0  9210  nn0lt2  9336  zneo  9356  uzind2  9367  fzind  9370  nn0ind-raph  9372  ledivge1le  9728  elfzmlbp  10134  difelfznle  10137  elfzodifsumelfzo  10203  ssfzo12  10226  flqeqceilz  10320  addmodlteq  10400  uzsinds  10444  qsqeqor  10633  facdiv  10720  facwordi  10722  bcpasc  10748  addcn2  11320  mulcn2  11322  climrecvg1n  11358  odd2np1  11880  oddge22np1  11888  gcdaddm  11987  algcvgblem  12051  cncongr1  12105  pcdvdsb  12321  pcaddlem  12340  infpnlem1  12359  prmunb  12362  imasaddfnlemg  12740  subrgdvds  13361  aprcotr  13380  metss2lem  14082  lgseisenlem2  14536  2sqlem6  14552