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  2905  sbciegft  3020  csbtt  3096  csbnestgf  3137  copsex2t  4279  pofun  4348  onsucmin  4544  onsucelsucr  4545  onsucsssucr  4546  ordsucunielexmid  4568  ordsuc  4600  nlimsucg  4603  elnn  4643  xpsspw  4776  elxp4  5158  elxp5  5159  funimass2  5337  imain  5341  funimaexg  5343  f1ff1  5474  dff1o2  5512  resdif  5529  funbrfv  5602  fvelimab  5620  eqfnfv2  5663  fvimacnvi  5679  ffvresb  5728  fnressn  5751  fmptapd  5756  fnex  5787  rexima  5804  ralima  5805  f1elima  5823  fnotovb  5969  mpoeq12  5986  fovcdm  6070  fnovrn  6075  ofrfval  6148  ofvalg  6149  cofunexg  6175  cofunex2g  6176  mpoexxg  6277  mpoexg  6278  f1o2ndf1  6295  spc2ed  6300  smodm2  6362  tfrlem9  6386  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  tfri3  6434  rdgtfr  6441  rdgruledefgg  6442  oav2  6530  oasuc  6531  omv2  6532  onasuc  6533  omsuc  6539  onmsuc  6540  nnaass  6552  nndi  6553  nndir  6557  nnaword  6578  ecelqsg  6656  iinerm  6675  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  fvdiagfn  6761  ixpssmap2g  6795  domentr  6859  xpdom1g  6901  fopwdom  6906  ssenen  6921  phplem3  6924  phplem4  6925  php5dom  6933  ssfilem  6945  diffitest  6957  ctssdccl  7186  pm54.43  7269  addclpi  7411  addasspig  7414  mulasspig  7416  distrpig  7417  mulcanpig  7419  nnppipi  7427  enqdc1  7446  addassnqg  7466  ltbtwnnqq  7499  prarloclemarch  7502  prarloclemarch2  7503  enq0sym  7516  enq0ref  7517  addclnq0  7535  nqpnq0nq  7537  nnanq0  7542  distrnq0  7543  addassnq0lemcl  7545  addassnq0  7546  distnq0r  7547  prarloclemlt  7577  genpassl  7608  genpassu  7609  genpassg  7610  nqpru  7636  addcomprg  7662  mulcomprg  7664  distrlem1prl  7666  distrlem1pru  7667  1idprl  7674  1idpru  7675  recexprlemdisj  7714  recexprlem1ssl  7717  peano2nnnn  7937  ax1rid  7961  axcaucvglemcl  7979  le2tri3i  8152  add4  8204  cnegexlem1  8218  cnegexlem3  8220  cnegex  8221  subadd  8246  addsub  8254  addsubeq4  8258  negdi  8300  renegcl  8304  resubcl  8307  subdi  8428  mulneg2  8439  mul2neg  8441  submul2  8442  ltnegcon2  8508  lenegcon2  8511  lesub0  8523  cru  8646  recextlem1  8695  recexap  8697  div12ap  8738  divnegap  8750  letrp1  8892  dfinfre  9000  peano2nn  9019  nndivre  9043  nnsub  9046  nndivtr  9049  arch  9263  bndndx  9265  nn0addge1  9312  nn0addge2  9313  zaddcl  9383  zsubcl  9384  zltnle  9389  zrevaddcl  9393  nzadd  9395  zleltp1  9398  zltlem1  9400  zdiv  9431  peano2uz2  9450  uzind  9454  eluzp1l  9643  ublbneg  9704  qaddcl  9726  qsubcl  9729  qreccl  9733  qdivcl  9734  qrevaddcl  9735  irradd  9737  irrmul  9738  rerpdivcl  9776  nn0ledivnn  9859  xrre  9912  rexsub  9945  xaddass  9961  xnpcan  9964  xsubge0  9973  xposdif  9974  elioc2  10028  icoshft  10082  iccdil  10090  fzss2  10156  fzsuc2  10171  fzrev2  10177  elfzm11  10183  elfzp1b  10189  fzrevral  10197  fzshftral  10200  fzof  10236  fzoval  10240  fzon  10259  fzosubel  10287  zpnn0elfzo  10300  elfzom1b  10322  qltnle  10350  flqlt  10390  flqbi  10397  flqaddz  10404  fzofig  10541  seq3feq2  10585  ser3le  10646  expp1  10655  expm1t  10676  expeq0  10679  binom2sub  10762  bernneq  10769  expnlbnd  10773  zzlesq  10817  faccl  10844  facdiv  10847  bcpasc  10875  bccl  10876  ffz0hash  10942  fnfzo0hash  10944  wrdlen1  10989  wrdred1  10994  2shfti  11013  crim  11040  mulreap  11046  resub  11052  imsub  11060  ipcnval  11068  cjsub  11074  resqrexlemfp1  11191  resqrexlemgt0  11202  sqabsadd  11237  sqabssub  11238  abs2dif2  11289  cau3lem  11296  icodiamlt  11362  xrmaxaddlem  11442  clim  11463  clim2  11465  clim2c  11466  clim0c  11468  2clim  11483  climabs0  11489  climcn1  11490  climcn2  11491  climsqz  11517  climsqz2  11518  climub  11526  climserle  11527  fsum3cvg  11560  fisumss  11574  fsum3ser  11579  sumsplitdc  11614  fsump1i  11615  fsumlessfi  11642  telfsumo  11648  fsumparts  11652  iserabs  11657  binomlem  11665  isumsplit  11673  isum1p  11674  isumlessdc  11678  mertenslem2  11718  mertensabs  11719  prodfap0  11727  prodfrecap  11728  prodfdivap  11729  fproddccvg  11754  prodmodclem2  11759  fprodssdc  11772  fprodabs  11798  fprodeq0  11799  fprodeq0g  11820  ege2le3  11853  efsub  11863  efexp  11864  efsep  11873  sinsub  11922  cossub  11923  demoivre  11955  eirraplem  11959  moddvds  11981  0dvds  11993  iddvdsexp  11997  dvdssub  12020  dvdsle  12026  dvdsleabs  12027  dvdseq  12030  dvdsflip  12033  mulsucdiv2z  12067  divalgb  12107  divalg2  12108  ndvdsadd  12113  bitsp1  12133  gcdneg  12174  gcdabs2  12182  modgcd  12183  bezoutlemsup  12201  gcdmultiplez  12213  gcdeq  12215  dvdssq  12223  lcmcllem  12260  lcmneg  12267  lcmdvds  12272  qredeu  12290  cncongrcoprm  12299  isprm3  12311  prmrp  12338  divnumden  12389  phiprmpw  12415  crth  12417  hashgcdlem  12431  hashgcdeq  12433  modprminv  12443  modprminveq  12444  modprmn0modprm0  12450  coprimeprodsq2  12452  pcpre1  12486  pccl  12493  pcmul  12495  pcdiv  12496  pcqcl  12500  pcexp  12503  pcdvds  12509  pcndvds  12511  pcndvds2  12513  pcelnn  12515  pcgcd1  12522  pc2dvds  12524  pc11  12525  gzsubcl  12574  4sqlem3  12584  setsresg  12741  pwssnf1o  13000  xpsfeq  13047  submcl  13181  grpinvnzcl  13274  mulgnnass  13363  nmzsubg  13416  nmznsg  13419  resghm2b  13468  ghmnsgpreima  13475  gsumfzsnfd  13551  iscrng2  13647  subrngpropd  13848  issubrg3  13879  subrgpropd  13885  islmodd  13925  lss1d  14015  lspsncl  14024  lspsnid  14039  df2idl2  14141  2idlcpbl  14156  qusrhm  14160  gsumfzfsumlemm  14219  iunopn  14322  unopn  14325  eltg  14372  eltg2  14373  tgcl  14384  tgiun  14393  tgidm  14394  isopn3i  14455  isneip  14466  neipsm  14474  restbasg  14488  restopn2  14503  lmbrf  14535  cnclima  14543  lmss  14566  txbasval  14587  txlm  14599  psmetxrge0  14652  blininf  14744  blssps  14747  blss  14748  elmopn2  14769  bdmet  14822  metrest  14826  bl2ioo  14870  dvcjbr  15028  plyaddlem1  15067  plymullem1  15068  plyreres  15084  dvply1  15085  dvply2g  15086  efper  15127  sinperlem  15128  abssinper  15166  cxpexprp  15215  logcxp  15217  rpcxpcl  15223  rpcxproot  15234  rprelogbmulexp  15276  lgsval2lem  15335  lgssq2  15366  lgsprme0  15367  bj-inex  15637  peano5set  15670  findset  15675  bj-findis  15709  nninfsellemsuc  15743  nninfself  15744  cvgcmp2nlemabs  15763  iooref1o  15765  trilpolemeq1  15771  nconstwlpolemgt0  15795