Theorem sylan2 284

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 275	. 2 |- ( ( ps /\ ph ) -> ch )
3		sylan2.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	syldan 280	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylan2b  285  sylan2br  286  syl2an  287  sylanr1  402  sylanr2  403  mpanr2  435  adantrl  470  adantrr  471  ancom2s  556  3adantr1  1146  3adantr2  1147  3adantr3  1148  syl3anr1  1280  syl3anr3  1282  dfbi3dc  1387  xordidc  1389  elabgt  2867  sbciegft  2981  csbtt  3057  csbnestgf  3097  copsex2t  4223  pofun  4290  onsucmin  4484  onsucelsucr  4485  onsucsssucr  4486  ordsucunielexmid  4508  ordsuc  4540  nlimsucg  4543  elnn  4583  xpsspw  4716  elxp4  5091  elxp5  5092  funimass2  5266  imain  5270  funimaexg  5272  f1ff1  5401  dff1o2  5437  resdif  5454  funbrfv  5525  fvelimab  5542  eqfnfv2  5584  fvimacnvi  5599  ffvresb  5648  fnressn  5671  fmptapd  5676  fnex  5707  rexima  5723  ralima  5724  f1elima  5741  fnotovb  5885  mpoeq12  5902  fovrn  5984  fnovrn  5989  ofrfval  6058  ofvalg  6059  cofunexg  6077  cofunex2g  6078  mpoexxg  6178  mpoexg  6179  f1o2ndf1  6196  spc2ed  6201  smodm2  6263  tfrlem9  6287  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  tfri3  6335  rdgtfr  6342  rdgruledefgg  6343  oav2  6431  oasuc  6432  omv2  6433  onasuc  6434  omsuc  6440  onmsuc  6441  nnaass  6453  nndi  6454  nndir  6458  nnaword  6479  ecelqsg  6554  iinerm  6573  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  fvdiagfn  6659  ixpssmap2g  6693  domentr  6757  xpdom1g  6799  fopwdom  6802  ssenen  6817  phplem3  6820  phplem4  6821  php5dom  6829  ssfilem  6841  diffitest  6853  ctssdccl  7076  pm54.43  7146  addclpi  7268  addasspig  7271  mulasspig  7273  distrpig  7274  mulcanpig  7276  nnppipi  7284  enqdc1  7303  addassnqg  7323  ltbtwnnqq  7356  prarloclemarch  7359  prarloclemarch2  7360  enq0sym  7373  enq0ref  7374  addclnq0  7392  nqpnq0nq  7394  nnanq0  7399  distrnq0  7400  addassnq0lemcl  7402  addassnq0  7403  distnq0r  7404  prarloclemlt  7434  genpassl  7465  genpassu  7466  genpassg  7467  nqpru  7493  addcomprg  7519  mulcomprg  7521  distrlem1prl  7523  distrlem1pru  7524  1idprl  7531  1idpru  7532  recexprlemdisj  7571  recexprlem1ssl  7574  peano2nnnn  7794  ax1rid  7818  axcaucvglemcl  7836  le2tri3i  8007  add4  8059  cnegexlem1  8073  cnegexlem3  8075  cnegex  8076  subadd  8101  addsub  8109  addsubeq4  8113  negdi  8155  renegcl  8159  resubcl  8162  subdi  8283  mulneg2  8294  mul2neg  8296  submul2  8297  ltnegcon2  8362  lenegcon2  8365  lesub0  8377  cru  8500  recextlem1  8548  recexap  8550  div12ap  8590  divnegap  8602  letrp1  8743  dfinfre  8851  peano2nn  8869  nndivre  8893  nnsub  8896  nndivtr  8899  arch  9111  bndndx  9113  nn0addge1  9160  nn0addge2  9161  zaddcl  9231  zsubcl  9232  zltnle  9237  zrevaddcl  9241  nzadd  9243  zleltp1  9246  zltlem1  9248  zdiv  9279  peano2uz2  9298  uzind  9302  eluzp1l  9490  ublbneg  9551  qaddcl  9573  qsubcl  9576  qreccl  9580  qdivcl  9581  qrevaddcl  9582  irradd  9584  irrmul  9585  rerpdivcl  9620  nn0ledivnn  9703  xrre  9756  rexsub  9789  xaddass  9805  xnpcan  9808  xsubge0  9817  xposdif  9818  elioc2  9872  icoshft  9926  iccdil  9934  fzss2  9999  fzsuc2  10014  fzrev2  10020  elfzm11  10026  elfzp1b  10032  fzrevral  10040  fzshftral  10043  fzof  10079  fzoval  10083  fzon  10101  fzosubel  10129  zpnn0elfzo  10142  elfzom1b  10164  qltnle  10181  flqlt  10218  flqbi  10225  flqaddz  10232  fzofig  10367  seq3feq2  10405  ser3le  10453  expp1  10462  expm1t  10483  expeq0  10486  binom2sub  10568  bernneq  10575  expnlbnd  10579  faccl  10648  facdiv  10651  bcpasc  10679  bccl  10680  ffz0hash  10746  fnfzo0hash  10748  2shfti  10773  crim  10800  mulreap  10806  resub  10812  imsub  10820  ipcnval  10828  cjsub  10834  resqrexlemfp1  10951  resqrexlemgt0  10962  sqabsadd  10997  sqabssub  10998  abs2dif2  11049  cau3lem  11056  icodiamlt  11122  xrmaxaddlem  11201  clim  11222  clim2  11224  clim2c  11225  clim0c  11227  2clim  11242  climabs0  11248  climcn1  11249  climcn2  11250  climsqz  11276  climsqz2  11277  climub  11285  climserle  11286  fsum3cvg  11319  fisumss  11333  fsum3ser  11338  sumsplitdc  11373  fsump1i  11374  fsumlessfi  11401  telfsumo  11407  fsumparts  11411  iserabs  11416  binomlem  11424  isumsplit  11432  isum1p  11433  isumlessdc  11437  mertenslem2  11477  mertensabs  11478  prodfap0  11486  prodfrecap  11487  prodfdivap  11488  fproddccvg  11513  prodmodclem2  11518  fprodssdc  11531  fprodabs  11557  fprodeq0  11558  fprodeq0g  11579  ege2le3  11612  efsub  11622  efexp  11623  efsep  11632  sinsub  11681  cossub  11682  demoivre  11713  eirraplem  11717  moddvds  11739  0dvds  11751  iddvdsexp  11755  dvdssub  11778  dvdsle  11782  dvdsleabs  11783  dvdseq  11786  dvdsflip  11789  mulsucdiv2z  11822  divalgb  11862  divalg2  11863  ndvdsadd  11868  gcdneg  11915  gcdabs2  11923  modgcd  11924  bezoutlemsup  11942  gcdmultiplez  11954  gcdeq  11956  dvdssq  11964  lcmcllem  11999  lcmneg  12006  lcmdvds  12011  qredeu  12029  cncongrcoprm  12038  isprm3  12050  prmrp  12077  divnumden  12128  phiprmpw  12154  crth  12156  hashgcdlem  12170  hashgcdeq  12171  modprminv  12181  modprminveq  12182  modprmn0modprm0  12188  coprimeprodsq2  12190  pcpre1  12224  pccl  12231  pcmul  12233  pcdiv  12234  pcqcl  12238  pcexp  12241  pcdvds  12246  pcndvds  12248  pcndvds2  12250  pcelnn  12252  pcgcd1  12259  pc2dvds  12261  pc11  12262  gzsubcl  12310  4sqlem3  12320  setsresg  12432  iunopn  12640  unopn  12643  eltg  12692  eltg2  12693  tgcl  12704  tgiun  12713  tgidm  12714  isopn3i  12775  isneip  12786  neipsm  12794  restbasg  12808  restopn2  12823  lmbrf  12855  cnclima  12863  lmss  12886  txbasval  12907  txlm  12919  psmetxrge0  12972  blininf  13064  blssps  13067  blss  13068  elmopn2  13089  bdmet  13142  metrest  13146  bl2ioo  13182  dvcjbr  13312  efper  13368  sinperlem  13369  abssinper  13407  cxpexprp  13456  logcxp  13458  rpcxpcl  13464  rpcxproot  13474  rprelogbmulexp  13514  lgsval2lem  13551  lgssq2  13582  lgsprme0  13583  bj-inex  13789  peano5set  13822  findset  13827  bj-findis  13861  nninfsellemsuc  13892  nninfself  13893  cvgcmp2nlemabs  13911  iooref1o  13913  trilpolemeq1  13919  nconstwlpolemgt0  13942