Theorem sylan2 286

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan2.1	|- ( ph -> ch )
sylan2.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 |- ( ph -> ch )
2	1	adantl 277	. 2 |- ( ( ps /\ ph ) -> ch )
3		sylan2.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	syldan 282	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

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 is referenced by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  404  sylanr2  405  mpanr2  438  adantrl  478  adantrr  479  ancom2s  566  3adantr1  1156  3adantr2  1157  3adantr3  1158  syl3anr1  1290  syl3anr3  1292  dfbi3dc  1397  xordidc  1399  elabgt  2880  sbciegft  2995  csbtt  3071  csbnestgf  3111  copsex2t  4247  pofun  4314  onsucmin  4508  onsucelsucr  4509  onsucsssucr  4510  ordsucunielexmid  4532  ordsuc  4564  nlimsucg  4567  elnn  4607  xpsspw  4740  elxp4  5118  elxp5  5119  funimass2  5296  imain  5300  funimaexg  5302  f1ff1  5431  dff1o2  5468  resdif  5485  funbrfv  5556  fvelimab  5574  eqfnfv2  5616  fvimacnvi  5632  ffvresb  5681  fnressn  5704  fmptapd  5709  fnex  5740  rexima  5757  ralima  5758  f1elima  5776  fnotovb  5920  mpoeq12  5937  fovcdm  6019  fnovrn  6024  ofrfval  6093  ofvalg  6094  cofunexg  6112  cofunex2g  6113  mpoexxg  6213  mpoexg  6214  f1o2ndf1  6231  spc2ed  6236  smodm2  6298  tfrlem9  6322  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  tfri3  6370  rdgtfr  6377  rdgruledefgg  6378  oav2  6466  oasuc  6467  omv2  6468  onasuc  6469  omsuc  6475  onmsuc  6476  nnaass  6488  nndi  6489  nndir  6493  nnaword  6514  ecelqsg  6590  iinerm  6609  ecovass  6646  ecoviass  6647  ecovdi  6648  ecovidi  6649  fvdiagfn  6695  ixpssmap2g  6729  domentr  6793  xpdom1g  6835  fopwdom  6838  ssenen  6853  phplem3  6856  phplem4  6857  php5dom  6865  ssfilem  6877  diffitest  6889  ctssdccl  7112  pm54.43  7191  addclpi  7328  addasspig  7331  mulasspig  7333  distrpig  7334  mulcanpig  7336  nnppipi  7344  enqdc1  7363  addassnqg  7383  ltbtwnnqq  7416  prarloclemarch  7419  prarloclemarch2  7420  enq0sym  7433  enq0ref  7434  addclnq0  7452  nqpnq0nq  7454  nnanq0  7459  distrnq0  7460  addassnq0lemcl  7462  addassnq0  7463  distnq0r  7464  prarloclemlt  7494  genpassl  7525  genpassu  7526  genpassg  7527  nqpru  7553  addcomprg  7579  mulcomprg  7581  distrlem1prl  7583  distrlem1pru  7584  1idprl  7591  1idpru  7592  recexprlemdisj  7631  recexprlem1ssl  7634  peano2nnnn  7854  ax1rid  7878  axcaucvglemcl  7896  le2tri3i  8068  add4  8120  cnegexlem1  8134  cnegexlem3  8136  cnegex  8137  subadd  8162  addsub  8170  addsubeq4  8174  negdi  8216  renegcl  8220  resubcl  8223  subdi  8344  mulneg2  8355  mul2neg  8357  submul2  8358  ltnegcon2  8423  lenegcon2  8426  lesub0  8438  cru  8561  recextlem1  8610  recexap  8612  div12ap  8653  divnegap  8665  letrp1  8807  dfinfre  8915  peano2nn  8933  nndivre  8957  nnsub  8960  nndivtr  8963  arch  9175  bndndx  9177  nn0addge1  9224  nn0addge2  9225  zaddcl  9295  zsubcl  9296  zltnle  9301  zrevaddcl  9305  nzadd  9307  zleltp1  9310  zltlem1  9312  zdiv  9343  peano2uz2  9362  uzind  9366  eluzp1l  9554  ublbneg  9615  qaddcl  9637  qsubcl  9640  qreccl  9644  qdivcl  9645  qrevaddcl  9646  irradd  9648  irrmul  9649  rerpdivcl  9686  nn0ledivnn  9769  xrre  9822  rexsub  9855  xaddass  9871  xnpcan  9874  xsubge0  9883  xposdif  9884  elioc2  9938  icoshft  9992  iccdil  10000  fzss2  10066  fzsuc2  10081  fzrev2  10087  elfzm11  10093  elfzp1b  10099  fzrevral  10107  fzshftral  10110  fzof  10146  fzoval  10150  fzon  10168  fzosubel  10196  zpnn0elfzo  10209  elfzom1b  10231  qltnle  10248  flqlt  10285  flqbi  10292  flqaddz  10299  fzofig  10434  seq3feq2  10472  ser3le  10520  expp1  10529  expm1t  10550  expeq0  10553  binom2sub  10636  bernneq  10643  expnlbnd  10647  faccl  10717  facdiv  10720  bcpasc  10748  bccl  10749  ffz0hash  10815  fnfzo0hash  10817  2shfti  10842  crim  10869  mulreap  10875  resub  10881  imsub  10889  ipcnval  10897  cjsub  10903  resqrexlemfp1  11020  resqrexlemgt0  11031  sqabsadd  11066  sqabssub  11067  abs2dif2  11118  cau3lem  11125  icodiamlt  11191  xrmaxaddlem  11270  clim  11291  clim2  11293  clim2c  11294  clim0c  11296  2clim  11311  climabs0  11317  climcn1  11318  climcn2  11319  climsqz  11345  climsqz2  11346  climub  11354  climserle  11355  fsum3cvg  11388  fisumss  11402  fsum3ser  11407  sumsplitdc  11442  fsump1i  11443  fsumlessfi  11470  telfsumo  11476  fsumparts  11480  iserabs  11485  binomlem  11493  isumsplit  11501  isum1p  11502  isumlessdc  11506  mertenslem2  11546  mertensabs  11547  prodfap0  11555  prodfrecap  11556  prodfdivap  11557  fproddccvg  11582  prodmodclem2  11587  fprodssdc  11600  fprodabs  11626  fprodeq0  11627  fprodeq0g  11648  ege2le3  11681  efsub  11691  efexp  11692  efsep  11701  sinsub  11750  cossub  11751  demoivre  11782  eirraplem  11786  moddvds  11808  0dvds  11820  iddvdsexp  11824  dvdssub  11847  dvdsle  11852  dvdsleabs  11853  dvdseq  11856  dvdsflip  11859  mulsucdiv2z  11892  divalgb  11932  divalg2  11933  ndvdsadd  11938  gcdneg  11985  gcdabs2  11993  modgcd  11994  bezoutlemsup  12012  gcdmultiplez  12024  gcdeq  12026  dvdssq  12034  lcmcllem  12069  lcmneg  12076  lcmdvds  12081  qredeu  12099  cncongrcoprm  12108  isprm3  12120  prmrp  12147  divnumden  12198  phiprmpw  12224  crth  12226  hashgcdlem  12240  hashgcdeq  12241  modprminv  12251  modprminveq  12252  modprmn0modprm0  12258  coprimeprodsq2  12260  pcpre1  12294  pccl  12301  pcmul  12303  pcdiv  12304  pcqcl  12308  pcexp  12311  pcdvds  12316  pcndvds  12318  pcndvds2  12320  pcelnn  12322  pcgcd1  12329  pc2dvds  12331  pc11  12332  gzsubcl  12380  4sqlem3  12390  setsresg  12502  xpsfeq  12769  submcl  12875  grpinvnzcl  12947  mulgnnass  13023  nmzsubg  13075  nmznsg  13078  iscrng2  13203  issubrg3  13373  subrgpropd  13374  islmodd  13388  lss1d  13475  iunopn  13541  unopn  13544  eltg  13591  eltg2  13592  tgcl  13603  tgiun  13612  tgidm  13613  isopn3i  13674  isneip  13685  neipsm  13693  restbasg  13707  restopn2  13722  lmbrf  13754  cnclima  13762  lmss  13785  txbasval  13806  txlm  13818  psmetxrge0  13871  blininf  13963  blssps  13966  blss  13967  elmopn2  13988  bdmet  14041  metrest  14045  bl2ioo  14081  dvcjbr  14211  efper  14267  sinperlem  14268  abssinper  14306  cxpexprp  14355  logcxp  14357  rpcxpcl  14363  rpcxproot  14373  rprelogbmulexp  14413  lgsval2lem  14450  lgssq2  14481  lgsprme0  14482  bj-inex  14698  peano5set  14731  findset  14736  bj-findis  14770  nninfsellemsuc  14800  nninfself  14801  cvgcmp2nlemabs  14819  iooref1o  14821  trilpolemeq1  14827  nconstwlpolemgt0  14850