Theorem sylbid 150

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

Hypotheses

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

Assertion

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

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 144	. 2 |- ( ph -> ( ps -> ch ) )
3		sylbid.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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4d  203  nlimsucg  4567  poltletr  5031  xp11m  5069  fvmptdf  5606  elfvmptrab1  5613  eusvobj2  5864  ovmpodf  6009  f1o2ndf1  6232  smoiso  6306  nnsseleq  6505  ecopovtrn  6635  ecopovtrng  6638  dom2lem  6775  fundmen  6809  fidifsnen  6873  findcard2  6892  findcard2s  6893  supisoex  7011  infglbti  7027  ordiso2  7037  updjud  7084  difinfsnlem  7101  enomnilem  7139  enmkvlem  7162  netap  7256  2omotaplemap  7259  cc2lem  7268  addcanpig  7336  mulcanpig  7337  addnidpig  7338  ordpipqqs  7376  ltexnqq  7410  prarloclemlo  7496  genpcdl  7521  genpcuu  7522  mulnqprl  7570  mulnqpru  7571  distrlem1prl  7584  distrlem1pru  7585  distrlem4prl  7586  distrlem4pru  7587  distrlem5prl  7588  distrlem5pru  7589  ltsopr  7598  ltexprlemfl  7611  ltexprlemfu  7613  recexprlemss1l  7637  recexprlemss1u  7638  aptiprleml  7641  ltsrprg  7749  lttrsr  7764  mulextsr1lem  7782  axapti  8031  cnegexlem1  8135  le2add  8404  lt2add  8405  ltleadd  8406  lt2sub  8420  le2sub  8421  recexre  8538  reapti  8539  apreap  8547  reapcotr  8558  remulext1  8559  apreim  8563  apcotr  8567  mulext2  8573  recexap  8613  addltmul  9158  elnnz  9266  zleloe  9303  difgtsumgt  9325  nn0n0n1ge2b  9335  nn0lt2  9337  nn0le2is012  9338  zextlt  9348  uzind2  9368  supinfneg  9598  infsupneg  9599  eluzdc  9613  qreccl  9645  elpq  9651  xltnegi  9838  xnn0lenn0nn0  9868  iccid  9928  icoshft  9993  zltaddlt1le  10010  fzofzim  10191  qbtwnxr  10261  flqeqceilz  10321  modqmuladdnn0  10371  modfzo0difsn  10398  addmodlteq  10401  frec2uzrand  10408  frecuzrdgtcl  10415  frecuzrdgfunlem  10422  facdiv  10721  facwordi  10723  faclbnd  10724  bcpasc  10749  seq3coll  10825  recvguniq  11007  abs00ap  11074  absext  11075  absnid  11085  cau3lem  11126  climuni  11304  2clim  11312  summodc  11394  fisumss  11403  fsumabs  11476  mertenslem2  11547  fprodssdc  11601  reeff1  11711  efieq1re  11782  dvdsmultr2  11843  dvdsleabs  11854  odd2np1lem  11880  odd2np1  11881  ltoddhalfle  11901  halfleoddlt  11902  m1expo  11908  nn0enne  11910  nn0ehalf  11911  nn0o1gt2  11913  flodddiv4  11942  zeqzmulgcd  11974  gcdneg  11986  gcdaddm  11988  bezoutlemaz  12007  bezoutlembz  12008  dfgcd2  12018  gcddiv  12023  dvdssqim  12028  algcvgblem  12052  algcvga  12054  lcmneg  12077  coprmgcdb  12091  coprmdvds2  12096  qredeq  12099  divgcdcoprm0  12104  divgcdcoprmex  12105  cncongr1  12106  cncongr2  12107  prmind2  12123  dvdsnprmd  12128  prmgt1  12135  nprmdvds1  12143  divgcdodd  12146  euclemma  12149  prmdvdsexpr  12153  prmfac1  12155  prmndvdsfaclt  12159  crth  12227  eulerthlemh  12234  fermltl  12237  nnnn0modprm0  12258  coprimeprodsq2  12261  pythagtriplem2  12269  pcpremul  12296  pcdvdsb  12322  pc2dvds  12332  pc11  12333  dvdsprmpweqnn  12338  dvdsprmpweqle  12339  difsqpwdvds  12340  pcfac  12351  oddprmdvds  12355  prmpwdvds  12356  1arith  12368  imasaddfnlemg  12741  erlecpbl  12758  xpsff1o  12775  grp1inv  12988  imasgrp2  12989  dvdsrtr  13308  dvdsrmul1  13309  unitgrp  13323  tgtop  13756  tgidm  13762  neipsm  13842  restbasg  13856  tgrest  13857  tgcn  13896  tgcnp  13897  cnconst2  13921  cnconst  13922  cnptopresti  13926  txbasval  13955  txcnp  13959  txdis1cn  13966  bldisj  14089  xblm  14105  blssps  14115  blss  14116  blin2  14120  cnlimcim  14328  dveflem  14375  sincosq3sgn  14437  sincosq4sgn  14438  coseq0q4123  14443  ioocosf1o  14463  logbgcd1irr  14573  zabsle1  14588  lgsdir2lem5  14621  lgsne0  14627  lgsdirnn0  14636  lgseisenlem2  14639  2lgsoddprmlem2  14642  uzdcinzz  14738  subctctexmid  14939