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  annimdc  939  3adantr1  1158  3adantr2  1159  3adantr3  1160  syl3anr1  1301  syl3anr3  1303  dfbi3dc  1408  xordidc  1410  elabgt  2902  sbciegft  3017  csbtt  3093  csbnestgf  3134  copsex2t  4275  pofun  4344  onsucmin  4540  onsucelsucr  4541  onsucsssucr  4542  ordsucunielexmid  4564  ordsuc  4596  nlimsucg  4599  elnn  4639  xpsspw  4772  elxp4  5154  elxp5  5155  funimass2  5333  imain  5337  funimaexg  5339  f1ff1  5468  dff1o2  5506  resdif  5523  funbrfv  5596  fvelimab  5614  eqfnfv2  5657  fvimacnvi  5673  ffvresb  5722  fnressn  5745  fmptapd  5750  fnex  5781  rexima  5798  ralima  5799  f1elima  5817  fnotovb  5962  mpoeq12  5979  fovcdm  6063  fnovrn  6068  ofrfval  6141  ofvalg  6142  cofunexg  6163  cofunex2g  6164  mpoexxg  6265  mpoexg  6266  f1o2ndf1  6283  spc2ed  6288  smodm2  6350  tfrlem9  6374  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  tfri3  6422  rdgtfr  6429  rdgruledefgg  6430  oav2  6518  oasuc  6519  omv2  6520  onasuc  6521  omsuc  6527  onmsuc  6528  nnaass  6540  nndi  6541  nndir  6545  nnaword  6566  ecelqsg  6644  iinerm  6663  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  fvdiagfn  6749  ixpssmap2g  6783  domentr  6847  xpdom1g  6889  fopwdom  6894  ssenen  6909  phplem3  6912  phplem4  6913  php5dom  6921  ssfilem  6933  diffitest  6945  ctssdccl  7172  pm54.43  7252  addclpi  7389  addasspig  7392  mulasspig  7394  distrpig  7395  mulcanpig  7397  nnppipi  7405  enqdc1  7424  addassnqg  7444  ltbtwnnqq  7477  prarloclemarch  7480  prarloclemarch2  7481  enq0sym  7494  enq0ref  7495  addclnq0  7513  nqpnq0nq  7515  nnanq0  7520  distrnq0  7521  addassnq0lemcl  7523  addassnq0  7524  distnq0r  7525  prarloclemlt  7555  genpassl  7586  genpassu  7587  genpassg  7588  nqpru  7614  addcomprg  7640  mulcomprg  7642  distrlem1prl  7644  distrlem1pru  7645  1idprl  7652  1idpru  7653  recexprlemdisj  7692  recexprlem1ssl  7695  peano2nnnn  7915  ax1rid  7939  axcaucvglemcl  7957  le2tri3i  8130  add4  8182  cnegexlem1  8196  cnegexlem3  8198  cnegex  8199  subadd  8224  addsub  8232  addsubeq4  8236  negdi  8278  renegcl  8282  resubcl  8285  subdi  8406  mulneg2  8417  mul2neg  8419  submul2  8420  ltnegcon2  8485  lenegcon2  8488  lesub0  8500  cru  8623  recextlem1  8672  recexap  8674  div12ap  8715  divnegap  8727  letrp1  8869  dfinfre  8977  peano2nn  8996  nndivre  9020  nnsub  9023  nndivtr  9026  arch  9240  bndndx  9242  nn0addge1  9289  nn0addge2  9290  zaddcl  9360  zsubcl  9361  zltnle  9366  zrevaddcl  9370  nzadd  9372  zleltp1  9375  zltlem1  9377  zdiv  9408  peano2uz2  9427  uzind  9431  eluzp1l  9620  ublbneg  9681  qaddcl  9703  qsubcl  9706  qreccl  9710  qdivcl  9711  qrevaddcl  9712  irradd  9714  irrmul  9715  rerpdivcl  9753  nn0ledivnn  9836  xrre  9889  rexsub  9922  xaddass  9938  xnpcan  9941  xsubge0  9950  xposdif  9951  elioc2  10005  icoshft  10059  iccdil  10067  fzss2  10133  fzsuc2  10148  fzrev2  10154  elfzm11  10160  elfzp1b  10166  fzrevral  10174  fzshftral  10177  fzof  10213  fzoval  10217  fzon  10236  fzosubel  10264  zpnn0elfzo  10277  elfzom1b  10299  qltnle  10316  flqlt  10355  flqbi  10362  flqaddz  10369  fzofig  10506  seq3feq2  10550  ser3le  10611  expp1  10620  expm1t  10641  expeq0  10644  binom2sub  10727  bernneq  10734  expnlbnd  10738  zzlesq  10782  faccl  10809  facdiv  10812  bcpasc  10840  bccl  10841  ffz0hash  10907  fnfzo0hash  10909  wrdlen1  10954  wrdred1  10959  2shfti  10978  crim  11005  mulreap  11011  resub  11017  imsub  11025  ipcnval  11033  cjsub  11039  resqrexlemfp1  11156  resqrexlemgt0  11167  sqabsadd  11202  sqabssub  11203  abs2dif2  11254  cau3lem  11261  icodiamlt  11327  xrmaxaddlem  11406  clim  11427  clim2  11429  clim2c  11430  clim0c  11432  2clim  11447  climabs0  11453  climcn1  11454  climcn2  11455  climsqz  11481  climsqz2  11482  climub  11490  climserle  11491  fsum3cvg  11524  fisumss  11538  fsum3ser  11543  sumsplitdc  11578  fsump1i  11579  fsumlessfi  11606  telfsumo  11612  fsumparts  11616  iserabs  11621  binomlem  11629  isumsplit  11637  isum1p  11638  isumlessdc  11642  mertenslem2  11682  mertensabs  11683  prodfap0  11691  prodfrecap  11692  prodfdivap  11693  fproddccvg  11718  prodmodclem2  11723  fprodssdc  11736  fprodabs  11762  fprodeq0  11763  fprodeq0g  11784  ege2le3  11817  efsub  11827  efexp  11828  efsep  11837  sinsub  11886  cossub  11887  demoivre  11919  eirraplem  11923  moddvds  11945  0dvds  11957  iddvdsexp  11961  dvdssub  11984  dvdsle  11989  dvdsleabs  11990  dvdseq  11993  dvdsflip  11996  mulsucdiv2z  12029  divalgb  12069  divalg2  12070  ndvdsadd  12075  gcdneg  12122  gcdabs2  12130  modgcd  12131  bezoutlemsup  12149  gcdmultiplez  12161  gcdeq  12163  dvdssq  12171  lcmcllem  12208  lcmneg  12215  lcmdvds  12220  qredeu  12238  cncongrcoprm  12247  isprm3  12259  prmrp  12286  divnumden  12337  phiprmpw  12363  crth  12365  hashgcdlem  12379  hashgcdeq  12380  modprminv  12390  modprminveq  12391  modprmn0modprm0  12397  coprimeprodsq2  12399  pcpre1  12433  pccl  12440  pcmul  12442  pcdiv  12443  pcqcl  12447  pcexp  12450  pcdvds  12456  pcndvds  12458  pcndvds2  12460  pcelnn  12462  pcgcd1  12469  pc2dvds  12471  pc11  12472  gzsubcl  12521  4sqlem3  12531  setsresg  12659  xpsfeq  12931  submcl  13054  grpinvnzcl  13147  mulgnnass  13230  nmzsubg  13283  nmznsg  13286  resghm2b  13335  ghmnsgpreima  13342  gsumfzsnfd  13418  iscrng2  13514  subrngpropd  13715  issubrg3  13746  subrgpropd  13752  islmodd  13792  lss1d  13882  lspsncl  13891  lspsnid  13906  df2idl2  14008  2idlcpbl  14023  qusrhm  14027  gsumfzfsumlemm  14086  iunopn  14181  unopn  14184  eltg  14231  eltg2  14232  tgcl  14243  tgiun  14252  tgidm  14253  isopn3i  14314  isneip  14325  neipsm  14333  restbasg  14347  restopn2  14362  lmbrf  14394  cnclima  14402  lmss  14425  txbasval  14446  txlm  14458  psmetxrge0  14511  blininf  14603  blssps  14606  blss  14607  elmopn2  14628  bdmet  14681  metrest  14685  bl2ioo  14729  dvcjbr  14887  plyaddlem1  14926  plymullem1  14927  plyreres  14942  dvply1  14943  efper  14983  sinperlem  14984  abssinper  15022  cxpexprp  15071  logcxp  15073  rpcxpcl  15079  rpcxproot  15089  rprelogbmulexp  15129  lgsval2lem  15167  lgssq2  15198  lgsprme0  15199  bj-inex  15469  peano5set  15502  findset  15507  bj-findis  15541  nninfsellemsuc  15572  nninfself  15573  cvgcmp2nlemabs  15592  iooref1o  15594  trilpolemeq1  15600  nconstwlpolemgt0  15624