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  2878  sbciegft  2993  csbtt  3069  csbnestgf  3109  copsex2t  4245  pofun  4312  onsucmin  4506  onsucelsucr  4507  onsucsssucr  4508  ordsucunielexmid  4530  ordsuc  4562  nlimsucg  4565  elnn  4605  xpsspw  4738  elxp4  5116  elxp5  5117  funimass2  5294  imain  5298  funimaexg  5300  f1ff1  5429  dff1o2  5466  resdif  5483  funbrfv  5554  fvelimab  5572  eqfnfv2  5614  fvimacnvi  5630  ffvresb  5679  fnressn  5702  fmptapd  5707  fnex  5738  rexima  5755  ralima  5756  f1elima  5773  fnotovb  5917  mpoeq12  5934  fovcdm  6016  fnovrn  6021  ofrfval  6090  ofvalg  6091  cofunexg  6109  cofunex2g  6110  mpoexxg  6210  mpoexg  6211  f1o2ndf1  6228  spc2ed  6233  smodm2  6295  tfrlem9  6319  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  tfri3  6367  rdgtfr  6374  rdgruledefgg  6375  oav2  6463  oasuc  6464  omv2  6465  onasuc  6466  omsuc  6472  onmsuc  6473  nnaass  6485  nndi  6486  nndir  6490  nnaword  6511  ecelqsg  6587  iinerm  6606  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  fvdiagfn  6692  ixpssmap2g  6726  domentr  6790  xpdom1g  6832  fopwdom  6835  ssenen  6850  phplem3  6853  phplem4  6854  php5dom  6862  ssfilem  6874  diffitest  6886  ctssdccl  7109  pm54.43  7188  addclpi  7325  addasspig  7328  mulasspig  7330  distrpig  7331  mulcanpig  7333  nnppipi  7341  enqdc1  7360  addassnqg  7380  ltbtwnnqq  7413  prarloclemarch  7416  prarloclemarch2  7417  enq0sym  7430  enq0ref  7431  addclnq0  7449  nqpnq0nq  7451  nnanq0  7456  distrnq0  7457  addassnq0lemcl  7459  addassnq0  7460  distnq0r  7461  prarloclemlt  7491  genpassl  7522  genpassu  7523  genpassg  7524  nqpru  7550  addcomprg  7576  mulcomprg  7578  distrlem1prl  7580  distrlem1pru  7581  1idprl  7588  1idpru  7589  recexprlemdisj  7628  recexprlem1ssl  7631  peano2nnnn  7851  ax1rid  7875  axcaucvglemcl  7893  le2tri3i  8064  add4  8116  cnegexlem1  8130  cnegexlem3  8132  cnegex  8133  subadd  8158  addsub  8166  addsubeq4  8170  negdi  8212  renegcl  8216  resubcl  8219  subdi  8340  mulneg2  8351  mul2neg  8353  submul2  8354  ltnegcon2  8419  lenegcon2  8422  lesub0  8434  cru  8557  recextlem1  8606  recexap  8608  div12ap  8649  divnegap  8661  letrp1  8803  dfinfre  8911  peano2nn  8929  nndivre  8953  nnsub  8956  nndivtr  8959  arch  9171  bndndx  9173  nn0addge1  9220  nn0addge2  9221  zaddcl  9291  zsubcl  9292  zltnle  9297  zrevaddcl  9301  nzadd  9303  zleltp1  9306  zltlem1  9308  zdiv  9339  peano2uz2  9358  uzind  9362  eluzp1l  9550  ublbneg  9611  qaddcl  9633  qsubcl  9636  qreccl  9640  qdivcl  9641  qrevaddcl  9642  irradd  9644  irrmul  9645  rerpdivcl  9682  nn0ledivnn  9765  xrre  9818  rexsub  9851  xaddass  9867  xnpcan  9870  xsubge0  9879  xposdif  9880  elioc2  9934  icoshft  9988  iccdil  9996  fzss2  10061  fzsuc2  10076  fzrev2  10082  elfzm11  10088  elfzp1b  10094  fzrevral  10102  fzshftral  10105  fzof  10141  fzoval  10145  fzon  10163  fzosubel  10191  zpnn0elfzo  10204  elfzom1b  10226  qltnle  10243  flqlt  10280  flqbi  10287  flqaddz  10294  fzofig  10429  seq3feq2  10467  ser3le  10515  expp1  10524  expm1t  10545  expeq0  10548  binom2sub  10630  bernneq  10637  expnlbnd  10641  faccl  10710  facdiv  10713  bcpasc  10741  bccl  10742  ffz0hash  10808  fnfzo0hash  10810  2shfti  10835  crim  10862  mulreap  10868  resub  10874  imsub  10882  ipcnval  10890  cjsub  10896  resqrexlemfp1  11013  resqrexlemgt0  11024  sqabsadd  11059  sqabssub  11060  abs2dif2  11111  cau3lem  11118  icodiamlt  11184  xrmaxaddlem  11263  clim  11284  clim2  11286  clim2c  11287  clim0c  11289  2clim  11304  climabs0  11310  climcn1  11311  climcn2  11312  climsqz  11338  climsqz2  11339  climub  11347  climserle  11348  fsum3cvg  11381  fisumss  11395  fsum3ser  11400  sumsplitdc  11435  fsump1i  11436  fsumlessfi  11463  telfsumo  11469  fsumparts  11473  iserabs  11478  binomlem  11486  isumsplit  11494  isum1p  11495  isumlessdc  11499  mertenslem2  11539  mertensabs  11540  prodfap0  11548  prodfrecap  11549  prodfdivap  11550  fproddccvg  11575  prodmodclem2  11580  fprodssdc  11593  fprodabs  11619  fprodeq0  11620  fprodeq0g  11641  ege2le3  11674  efsub  11684  efexp  11685  efsep  11694  sinsub  11743  cossub  11744  demoivre  11775  eirraplem  11779  moddvds  11801  0dvds  11813  iddvdsexp  11817  dvdssub  11840  dvdsle  11844  dvdsleabs  11845  dvdseq  11848  dvdsflip  11851  mulsucdiv2z  11884  divalgb  11924  divalg2  11925  ndvdsadd  11930  gcdneg  11977  gcdabs2  11985  modgcd  11986  bezoutlemsup  12004  gcdmultiplez  12016  gcdeq  12018  dvdssq  12026  lcmcllem  12061  lcmneg  12068  lcmdvds  12073  qredeu  12091  cncongrcoprm  12100  isprm3  12112  prmrp  12139  divnumden  12190  phiprmpw  12216  crth  12218  hashgcdlem  12232  hashgcdeq  12233  modprminv  12243  modprminveq  12244  modprmn0modprm0  12250  coprimeprodsq2  12252  pcpre1  12286  pccl  12293  pcmul  12295  pcdiv  12296  pcqcl  12300  pcexp  12303  pcdvds  12308  pcndvds  12310  pcndvds2  12312  pcelnn  12314  pcgcd1  12321  pc2dvds  12323  pc11  12324  gzsubcl  12372  4sqlem3  12382  setsresg  12494  submcl  12824  grpinvnzcl  12896  mulgnnass  12971  nmzsubg  13023  nmznsg  13026  iscrng2  13151  issubrg3  13328  subrgpropd  13329  iunopn  13393  unopn  13396  eltg  13445  eltg2  13446  tgcl  13457  tgiun  13466  tgidm  13467  isopn3i  13528  isneip  13539  neipsm  13547  restbasg  13561  restopn2  13576  lmbrf  13608  cnclima  13616  lmss  13639  txbasval  13660  txlm  13672  psmetxrge0  13725  blininf  13817  blssps  13820  blss  13821  elmopn2  13842  bdmet  13895  metrest  13899  bl2ioo  13935  dvcjbr  14065  efper  14121  sinperlem  14122  abssinper  14160  cxpexprp  14209  logcxp  14211  rpcxpcl  14217  rpcxproot  14227  rprelogbmulexp  14267  lgsval2lem  14304  lgssq2  14335  lgsprme0  14336  bj-inex  14541  peano5set  14574  findset  14579  bj-findis  14613  nninfsellemsuc  14643  nninfself  14644  cvgcmp2nlemabs  14662  iooref1o  14664  trilpolemeq1  14670  nconstwlpolemgt0  14693