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  568  annimdc  946  ifpnst  997  3adantr1  1183  3adantr2  1184  3adantr3  1185  syl3anr1  1326  syl3anr3  1328  dfbi3dc  1442  xordidc  1444  elabgt  2961  sbciegft  3076  csbtt  3153  csbnestgf  3194  copsex2t  4366  pofun  4438  onsucmin  4634  onsucelsucr  4635  onsucsssucr  4636  ordsucunielexmid  4658  ordsuc  4690  nlimsucg  4693  elnn  4733  xpsspw  4867  elxp4  5255  elxp5  5256  funimass2  5439  imain  5443  funimaexg  5445  f1ff1  5586  dff1o2  5624  resdif  5641  funbrfv  5718  fnbrfvb2  5724  fvelimab  5738  eqfnfv2  5781  fvimacnvi  5797  ffvresb  5845  fnressn  5875  fmptapd  5880  fnex  5911  rexima  5933  ralima  5934  f1elima  5952  fnotovb  6104  mpoeq12  6121  fovcdm  6205  fnovrn  6210  ofrfval  6284  ofvalg  6285  cofunexg  6311  cofunex2g  6312  mpoexxg  6419  mpoexg  6420  f1o2ndf1  6437  spc2ed  6442  funsssuppss  6471  smodm2  6539  tfrlem9  6563  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  tfri3  6611  rdgtfr  6618  rdgruledefgg  6619  oav2  6709  oasuc  6710  omv2  6711  onasuc  6712  omsuc  6718  onmsuc  6719  nnaass  6731  nndi  6732  nndir  6736  nnaword  6757  ecelqsg  6835  iinerm  6854  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  fvdiagfn  6941  ixpssmap2g  6975  domentr  7044  xpdom1g  7097  fopwdom  7102  ssenen  7118  phplem3  7121  phplem4  7122  php5dom  7130  ssfilem  7143  ssfilemd  7145  diffitest  7157  ctssdccl  7415  pm54.43  7500  pw1if  7548  addclpi  7658  addasspig  7661  mulasspig  7663  distrpig  7664  mulcanpig  7666  nnppipi  7674  enqdc1  7693  addassnqg  7713  ltbtwnnqq  7746  prarloclemarch  7749  prarloclemarch2  7750  enq0sym  7763  enq0ref  7764  addclnq0  7782  nqpnq0nq  7784  nnanq0  7789  distrnq0  7790  addassnq0lemcl  7792  addassnq0  7793  distnq0r  7794  prarloclemlt  7824  genpassl  7855  genpassu  7856  genpassg  7857  nqpru  7883  addcomprg  7909  mulcomprg  7911  distrlem1prl  7913  distrlem1pru  7914  1idprl  7921  1idpru  7922  recexprlemdisj  7961  recexprlem1ssl  7964  peano2nnnn  8184  ax1rid  8208  axcaucvglemcl  8226  le2tri3i  8398  add4  8450  cnegexlem1  8464  cnegexlem3  8466  cnegex  8467  subadd  8492  addsub  8500  addsubeq4  8504  negdi  8546  renegcl  8550  resubcl  8553  subdi  8675  mulneg2  8686  mul2neg  8688  submul2  8689  ltnegcon2  8755  lenegcon2  8758  lesub0  8770  cru  8893  recextlem1  8942  recexap  8944  div12ap  8985  divnegap  8997  letrp1  9139  dfinfre  9247  peano2nn  9266  nndivre  9290  nnsub  9293  nndivtr  9296  arch  9510  bndndx  9512  nn0addge1  9559  nn0addge2  9560  zaddcl  9634  zsubcl  9635  zltnle  9640  zrevaddcl  9645  nzadd  9647  zleltp1  9650  zltlem1  9652  zdiv  9684  peano2uz2  9703  uzind  9707  eluzp1l  9897  ublbneg  9963  qaddcl  9985  qsubcl  9988  qreccl  9992  qdivcl  9993  qrevaddcl  9994  irradd  9996  irrmul  9997  rerpdivcl  10035  nn0ledivnn  10118  xrre  10172  rexsub  10205  xaddass  10221  xnpcan  10224  xsubge0  10233  xposdif  10234  elioc2  10288  icoshft  10342  iccdil  10350  fzss2  10419  fzsuc2  10435  fzrev2  10441  elfzm11  10447  elfzp1b  10453  fzrevral  10461  fzshftral  10464  fzof  10500  fzoval  10504  fzon  10523  elfzoextl  10558  fzosubel  10561  zpnn0elfzo  10574  elfzom1b  10596  qltnle  10627  flqlt  10667  flqbi  10674  flqaddz  10681  fzofig  10818  seq3feq2  10862  ser3le  10923  expp1  10932  expm1t  10953  expeq0  10956  binom2sub  11039  bernneq  11047  expnlbnd  11051  zzlesq  11095  faccl  11122  facdiv  11125  bcpasc  11153  bccl  11154  ffz0hash  11225  fnfzo0hash  11227  hashfibclem  11231  wrdlen1  11287  wrdred1  11292  ccatval21sw  11318  wrdl1exs1  11342  ccatws1cl  11345  ccatws1leng  11347  pfxmpt  11397  pfxfv  11401  pfxfvlsw  11412  ccatpfx  11418  pfx1  11420  swrdccatin1  11442  swrdccat  11452  pfxccatpfx1  11453  2shfti  11541  crim  11568  mulreap  11574  resub  11580  imsub  11588  ipcnval  11596  cjsub  11602  resqrexlemfp1  11719  resqrexlemgt0  11730  sqabsadd  11765  sqabssub  11766  abs2dif2  11817  cau3lem  11824  icodiamlt  11890  xrmaxaddlem  11970  clim  11991  clim2  11993  clim2c  11994  clim0c  11996  2clim  12011  climabs0  12017  climcn1  12018  climcn2  12019  climsqz  12045  climsqz2  12046  climub  12054  climserle  12055  fsum3cvg  12089  fisumss  12103  fsum3ser  12108  sumsplitdc  12143  fsump1i  12144  fsumlessfi  12171  telfsumo  12177  fsumparts  12181  iserabs  12186  binomlem  12194  isumsplit  12202  isum1p  12203  isumlessdc  12207  mertenslem2  12247  mertensabs  12248  prodfap0  12256  prodfrecap  12257  prodfdivap  12258  fproddccvg  12283  prodmodclem2  12288  fprodssdc  12301  fprodabs  12327  fprodeq0  12328  fprodeq0g  12349  ege2le3  12382  efsub  12392  efexp  12393  efsep  12402  sinsub  12451  cossub  12452  demoivre  12484  eirraplem  12488  moddvds  12510  0dvds  12522  iddvdsexp  12526  dvdssub  12549  dvdsle  12555  dvdsleabs  12556  dvdseq  12559  dvdsflip  12562  mulsucdiv2z  12596  divalgb  12636  divalg2  12637  ndvdsadd  12642  bitsp1  12662  gcdneg  12703  gcdabs2  12711  modgcd  12712  bezoutlemsup  12730  gcdmultiplez  12742  gcdeq  12744  dvdssq  12752  lcmcllem  12789  lcmneg  12796  lcmdvds  12801  qredeu  12819  cncongrcoprm  12828  isprm3  12840  prmrp  12867  divnumden  12918  phiprmpw  12944  crth  12946  hashgcdlem  12960  hashgcdeq  12962  modprminv  12972  modprminveq  12973  modprmn0modprm0  12979  coprimeprodsq2  12981  pcpre1  13015  pccl  13022  pcmul  13024  pcdiv  13025  pcqcl  13029  pcexp  13032  pcdvds  13038  pcndvds  13040  pcndvds2  13042  pcelnn  13044  pcgcd1  13051  pc2dvds  13053  pc11  13054  gzsubcl  13103  4sqlem3  13113  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemfrceq  13216  setsresg  13334  xpsfeq  13609  submcl  13734  grpinvnzcl  13827  mulgnnass  13910  nmzsubg  13963  nmznsg  13966  resghm2b  14015  ghmnsgpreima  14022  gsumfzsnfd  14098  pwssnf1o  14153  iscrng2  14258  subrngpropd  14462  issubrg3  14493  subrgpropd  14499  islmodd  14567  lss1d  14657  lspsncl  14666  lspsnid  14681  df2idl2  14783  2idlcpbl  14798  qusrhm  14802  gsumfzfsumlemm  14861  iunopn  14993  unopn  14996  eltg  15043  eltg2  15044  tgcl  15055  tgiun  15064  tgidm  15065  isopn3i  15126  isneip  15137  neipsm  15145  restbasg  15159  restopn2  15174  lmbrf  15206  cnclima  15214  lmss  15237  txbasval  15258  txlm  15270  psmetxrge0  15323  blininf  15415  blssps  15418  blss  15419  elmopn2  15440  bdmet  15493  metrest  15497  bl2ioo  15541  dvcjbr  15699  plyaddlem1  15738  plymullem1  15739  plyreres  15755  dvply1  15756  dvply2g  15757  efper  15798  sinperlem  15799  abssinper  15837  cxpexprp  15886  logcxp  15888  rpcxpcl  15894  rpcxproot  15905  rprelogbmulexp  15947  lgsval2lem  16009  lgssq2  16040  lgsprme0  16041  ausgrusgrben  16289  wlkepvtx  16496  bj-inex  16803  peano5set  16836  findset  16841  bj-findis  16875  nninfsellemsuc  16916  nninfself  16917  cvgcmp2nlemabs  16942  iooref1o  16944  trilpolemeq1  16950  nconstwlpolemgt0  16976