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  2958  sbciegft  3073  csbtt  3150  csbnestgf  3191  copsex2t  4361  pofun  4433  onsucmin  4629  onsucelsucr  4630  onsucsssucr  4631  ordsucunielexmid  4653  ordsuc  4685  nlimsucg  4688  elnn  4728  xpsspw  4862  elxp4  5250  elxp5  5251  funimass2  5434  imain  5438  funimaexg  5440  f1ff1  5581  dff1o2  5619  resdif  5636  funbrfv  5713  fnbrfvb2  5719  fvelimab  5733  eqfnfv2  5776  fvimacnvi  5792  ffvresb  5840  fnressn  5870  fmptapd  5875  fnex  5906  rexima  5927  ralima  5928  f1elima  5946  fnotovb  6096  mpoeq12  6113  fovcdm  6197  fnovrn  6202  ofrfval  6275  ofvalg  6276  cofunexg  6302  cofunex2g  6303  mpoexxg  6406  mpoexg  6407  f1o2ndf1  6424  spc2ed  6429  funsssuppss  6458  smodm2  6526  tfrlem9  6550  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  tfri3  6598  rdgtfr  6605  rdgruledefgg  6606  oav2  6696  oasuc  6697  omv2  6698  onasuc  6699  omsuc  6705  onmsuc  6706  nnaass  6718  nndi  6719  nndir  6723  nnaword  6744  ecelqsg  6822  iinerm  6841  ecovass  6878  ecoviass  6879  ecovdi  6880  ecovidi  6881  fvdiagfn  6928  ixpssmap2g  6962  domentr  7031  xpdom1g  7084  fopwdom  7089  ssenen  7105  phplem3  7108  phplem4  7109  php5dom  7117  ssfilem  7130  ssfilemd  7132  diffitest  7144  ctssdccl  7402  pm54.43  7487  pw1if  7535  addclpi  7642  addasspig  7645  mulasspig  7647  distrpig  7648  mulcanpig  7650  nnppipi  7658  enqdc1  7677  addassnqg  7697  ltbtwnnqq  7730  prarloclemarch  7733  prarloclemarch2  7734  enq0sym  7747  enq0ref  7748  addclnq0  7766  nqpnq0nq  7768  nnanq0  7773  distrnq0  7774  addassnq0lemcl  7776  addassnq0  7777  distnq0r  7778  prarloclemlt  7808  genpassl  7839  genpassu  7840  genpassg  7841  nqpru  7867  addcomprg  7893  mulcomprg  7895  distrlem1prl  7897  distrlem1pru  7898  1idprl  7905  1idpru  7906  recexprlemdisj  7945  recexprlem1ssl  7948  peano2nnnn  8168  ax1rid  8192  axcaucvglemcl  8210  le2tri3i  8382  add4  8434  cnegexlem1  8448  cnegexlem3  8450  cnegex  8451  subadd  8476  addsub  8484  addsubeq4  8488  negdi  8530  renegcl  8534  resubcl  8537  subdi  8658  mulneg2  8669  mul2neg  8671  submul2  8672  ltnegcon2  8738  lenegcon2  8741  lesub0  8753  cru  8876  recextlem1  8925  recexap  8927  div12ap  8968  divnegap  8980  letrp1  9122  dfinfre  9230  peano2nn  9249  nndivre  9273  nnsub  9276  nndivtr  9279  arch  9493  bndndx  9495  nn0addge1  9542  nn0addge2  9543  zaddcl  9617  zsubcl  9618  zltnle  9623  zrevaddcl  9628  nzadd  9630  zleltp1  9633  zltlem1  9635  zdiv  9666  peano2uz2  9685  uzind  9689  eluzp1l  9879  ublbneg  9945  qaddcl  9967  qsubcl  9970  qreccl  9974  qdivcl  9975  qrevaddcl  9976  irradd  9978  irrmul  9979  rerpdivcl  10017  nn0ledivnn  10100  xrre  10153  rexsub  10186  xaddass  10202  xnpcan  10205  xsubge0  10214  xposdif  10215  elioc2  10269  icoshft  10323  iccdil  10331  fzss2  10398  fzsuc2  10413  fzrev2  10419  elfzm11  10425  elfzp1b  10431  fzrevral  10439  fzshftral  10442  fzof  10478  fzoval  10482  fzon  10501  elfzoextl  10536  fzosubel  10539  zpnn0elfzo  10552  elfzom1b  10574  qltnle  10603  flqlt  10643  flqbi  10650  flqaddz  10657  fzofig  10794  seq3feq2  10838  ser3le  10899  expp1  10908  expm1t  10929  expeq0  10932  binom2sub  11015  bernneq  11022  expnlbnd  11026  zzlesq  11070  faccl  11097  facdiv  11100  bcpasc  11128  bccl  11129  ffz0hash  11200  fnfzo0hash  11202  hashfibclem  11206  wrdlen1  11262  wrdred1  11267  ccatval21sw  11293  wrdl1exs1  11317  ccatws1cl  11320  ccatws1leng  11322  pfxmpt  11372  pfxfv  11376  pfxfvlsw  11387  ccatpfx  11393  pfx1  11395  swrdccatin1  11417  swrdccat  11427  pfxccatpfx1  11428  2shfti  11516  crim  11543  mulreap  11549  resub  11555  imsub  11563  ipcnval  11571  cjsub  11577  resqrexlemfp1  11694  resqrexlemgt0  11705  sqabsadd  11740  sqabssub  11741  abs2dif2  11792  cau3lem  11799  icodiamlt  11865  xrmaxaddlem  11945  clim  11966  clim2  11968  clim2c  11969  clim0c  11971  2clim  11986  climabs0  11992  climcn1  11993  climcn2  11994  climsqz  12020  climsqz2  12021  climub  12029  climserle  12030  fsum3cvg  12064  fisumss  12078  fsum3ser  12083  sumsplitdc  12118  fsump1i  12119  fsumlessfi  12146  telfsumo  12152  fsumparts  12156  iserabs  12161  binomlem  12169  isumsplit  12177  isum1p  12178  isumlessdc  12182  mertenslem2  12222  mertensabs  12223  prodfap0  12231  prodfrecap  12232  prodfdivap  12233  fproddccvg  12258  prodmodclem2  12263  fprodssdc  12276  fprodabs  12302  fprodeq0  12303  fprodeq0g  12324  ege2le3  12357  efsub  12367  efexp  12368  efsep  12377  sinsub  12426  cossub  12427  demoivre  12459  eirraplem  12463  moddvds  12485  0dvds  12497  iddvdsexp  12501  dvdssub  12524  dvdsle  12530  dvdsleabs  12531  dvdseq  12534  dvdsflip  12537  mulsucdiv2z  12571  divalgb  12611  divalg2  12612  ndvdsadd  12617  bitsp1  12637  gcdneg  12678  gcdabs2  12686  modgcd  12687  bezoutlemsup  12705  gcdmultiplez  12717  gcdeq  12719  dvdssq  12727  lcmcllem  12764  lcmneg  12771  lcmdvds  12776  qredeu  12794  cncongrcoprm  12803  isprm3  12815  prmrp  12842  divnumden  12893  phiprmpw  12919  crth  12921  hashgcdlem  12935  hashgcdeq  12937  modprminv  12947  modprminveq  12948  modprmn0modprm0  12954  coprimeprodsq2  12956  pcpre1  12990  pccl  12997  pcmul  12999  pcdiv  13000  pcqcl  13004  pcexp  13007  pcdvds  13013  pcndvds  13015  pcndvds2  13017  pcelnn  13019  pcgcd1  13026  pc2dvds  13028  pc11  13029  gzsubcl  13078  4sqlem3  13088  setsresg  13250  pwssnf1o  13511  xpsfeq  13558  submcl  13692  grpinvnzcl  13785  mulgnnass  13874  nmzsubg  13927  nmznsg  13930  resghm2b  13979  ghmnsgpreima  13986  gsumfzsnfd  14062  iscrng2  14159  subrngpropd  14361  issubrg3  14392  subrgpropd  14398  islmodd  14441  lss1d  14531  lspsncl  14540  lspsnid  14555  df2idl2  14657  2idlcpbl  14672  qusrhm  14676  gsumfzfsumlemm  14735  iunopn  14867  unopn  14870  eltg  14917  eltg2  14918  tgcl  14929  tgiun  14938  tgidm  14939  isopn3i  15000  isneip  15011  neipsm  15019  restbasg  15033  restopn2  15048  lmbrf  15080  cnclima  15088  lmss  15111  txbasval  15132  txlm  15144  psmetxrge0  15197  blininf  15289  blssps  15292  blss  15293  elmopn2  15314  bdmet  15367  metrest  15371  bl2ioo  15415  dvcjbr  15573  plyaddlem1  15612  plymullem1  15613  plyreres  15629  dvply1  15630  dvply2g  15631  efper  15672  sinperlem  15673  abssinper  15711  cxpexprp  15760  logcxp  15762  rpcxpcl  15768  rpcxproot  15779  rprelogbmulexp  15821  lgsval2lem  15883  lgssq2  15914  lgsprme0  15915  ausgrusgrben  16163  wlkepvtx  16370  bj-inex  16677  peano5set  16710  findset  16715  bj-findis  16749  nninfsellemsuc  16790  nninfself  16791  cvgcmp2nlemabs  16816  iooref1o  16818  trilpolemeq1  16824  nconstwlpolemgt0  16850