Theorem sylbird 170

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

Hypotheses

Ref	Expression
sylbird.1	|- ( ph -> ( ch <-> ps ) )
sylbird.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
sylbird	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 |- ( ph -> ( ch <-> ps ) )
2	1	biimprd 158	. 2 |- ( ph -> ( ps -> ch ) )
3		sylbird.2	. 2 |- ( ph -> ( ch -> th ) )
4	2, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

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  1822  eqreu  2969  onsucsssucr  4565  ordsucunielexmid  4587  ovi3  6096  tfrlem9  6418  dom2lem  6876  distrlem4prl  7717  distrlem4pru  7718  recexprlemm  7757  caucvgprlem1  7812  caucvgprprlemexb  7840  aptisr  7912  map2psrprg  7938  renegcl  8353  addid0  8465  remulext2  8693  mulext1  8705  apmul1  8881  nnge1  9079  0mnnnnn0  9347  nn0lt2  9474  zneo  9494  uzind2  9505  fzind  9508  nn0ind-raph  9510  ledivge1le  9868  elfzmlbp  10274  difelfznle  10277  elfzodifsumelfzo  10352  ssfzo12  10375  flqeqceilz  10485  addmodlteq  10565  uzsinds  10611  qsqeqor  10817  facdiv  10905  facwordi  10907  bcpasc  10933  ccatsymb  11081  swrdsbslen  11142  swrdspsleq  11143  swrdlsw  11145  swrdswrdlem  11180  addcn2  11696  mulcn2  11698  climrecvg1n  11734  odd2np1  12259  oddge22np1  12267  bitsfzo  12341  gcdaddm  12380  algcvgblem  12446  cncongr1  12500  pcdvdsb  12718  pcaddlem  12737  infpnlem1  12757  prmunb  12760  imasaddfnlemg  13221  f1ghm0to0  13683  ghmf1  13684  imasring  13901  subrgdvds  14072  aprcotr  14122  quscrng  14370  metss2lem  15044  gausslemma2dlem0i  15609  gausslemma2dlem1a  15610  lgseisenlem2  15623  2sqlem6  15672  incistruhgr  15761