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  436  adantrl  475  adantrr  476  ancom2s  561  3adantr1  1151  3adantr2  1152  3adantr3  1153  syl3anr1  1285  syl3anr3  1287  dfbi3dc  1392  xordidc  1394  elabgt  2871  sbciegft  2985  csbtt  3061  csbnestgf  3101  copsex2t  4230  pofun  4297  onsucmin  4491  onsucelsucr  4492  onsucsssucr  4493  ordsucunielexmid  4515  ordsuc  4547  nlimsucg  4550  elnn  4590  xpsspw  4723  elxp4  5098  elxp5  5099  funimass2  5276  imain  5280  funimaexg  5282  f1ff1  5411  dff1o2  5447  resdif  5464  funbrfv  5535  fvelimab  5552  eqfnfv2  5594  fvimacnvi  5610  ffvresb  5659  fnressn  5682  fmptapd  5687  fnex  5718  rexima  5734  ralima  5735  f1elima  5752  fnotovb  5896  mpoeq12  5913  fovrn  5995  fnovrn  6000  ofrfval  6069  ofvalg  6070  cofunexg  6088  cofunex2g  6089  mpoexxg  6189  mpoexg  6190  f1o2ndf1  6207  spc2ed  6212  smodm2  6274  tfrlem9  6298  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  tfri3  6346  rdgtfr  6353  rdgruledefgg  6354  oav2  6442  oasuc  6443  omv2  6444  onasuc  6445  omsuc  6451  onmsuc  6452  nnaass  6464  nndi  6465  nndir  6469  nnaword  6490  ecelqsg  6566  iinerm  6585  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  fvdiagfn  6671  ixpssmap2g  6705  domentr  6769  xpdom1g  6811  fopwdom  6814  ssenen  6829  phplem3  6832  phplem4  6833  php5dom  6841  ssfilem  6853  diffitest  6865  ctssdccl  7088  pm54.43  7167  addclpi  7289  addasspig  7292  mulasspig  7294  distrpig  7295  mulcanpig  7297  nnppipi  7305  enqdc1  7324  addassnqg  7344  ltbtwnnqq  7377  prarloclemarch  7380  prarloclemarch2  7381  enq0sym  7394  enq0ref  7395  addclnq0  7413  nqpnq0nq  7415  nnanq0  7420  distrnq0  7421  addassnq0lemcl  7423  addassnq0  7424  distnq0r  7425  prarloclemlt  7455  genpassl  7486  genpassu  7487  genpassg  7488  nqpru  7514  addcomprg  7540  mulcomprg  7542  distrlem1prl  7544  distrlem1pru  7545  1idprl  7552  1idpru  7553  recexprlemdisj  7592  recexprlem1ssl  7595  peano2nnnn  7815  ax1rid  7839  axcaucvglemcl  7857  le2tri3i  8028  add4  8080  cnegexlem1  8094  cnegexlem3  8096  cnegex  8097  subadd  8122  addsub  8130  addsubeq4  8134  negdi  8176  renegcl  8180  resubcl  8183  subdi  8304  mulneg2  8315  mul2neg  8317  submul2  8318  ltnegcon2  8383  lenegcon2  8386  lesub0  8398  cru  8521  recextlem1  8569  recexap  8571  div12ap  8611  divnegap  8623  letrp1  8764  dfinfre  8872  peano2nn  8890  nndivre  8914  nnsub  8917  nndivtr  8920  arch  9132  bndndx  9134  nn0addge1  9181  nn0addge2  9182  zaddcl  9252  zsubcl  9253  zltnle  9258  zrevaddcl  9262  nzadd  9264  zleltp1  9267  zltlem1  9269  zdiv  9300  peano2uz2  9319  uzind  9323  eluzp1l  9511  ublbneg  9572  qaddcl  9594  qsubcl  9597  qreccl  9601  qdivcl  9602  qrevaddcl  9603  irradd  9605  irrmul  9606  rerpdivcl  9641  nn0ledivnn  9724  xrre  9777  rexsub  9810  xaddass  9826  xnpcan  9829  xsubge0  9838  xposdif  9839  elioc2  9893  icoshft  9947  iccdil  9955  fzss2  10020  fzsuc2  10035  fzrev2  10041  elfzm11  10047  elfzp1b  10053  fzrevral  10061  fzshftral  10064  fzof  10100  fzoval  10104  fzon  10122  fzosubel  10150  zpnn0elfzo  10163  elfzom1b  10185  qltnle  10202  flqlt  10239  flqbi  10246  flqaddz  10253  fzofig  10388  seq3feq2  10426  ser3le  10474  expp1  10483  expm1t  10504  expeq0  10507  binom2sub  10589  bernneq  10596  expnlbnd  10600  faccl  10669  facdiv  10672  bcpasc  10700  bccl  10701  ffz0hash  10768  fnfzo0hash  10770  2shfti  10795  crim  10822  mulreap  10828  resub  10834  imsub  10842  ipcnval  10850  cjsub  10856  resqrexlemfp1  10973  resqrexlemgt0  10984  sqabsadd  11019  sqabssub  11020  abs2dif2  11071  cau3lem  11078  icodiamlt  11144  xrmaxaddlem  11223  clim  11244  clim2  11246  clim2c  11247  clim0c  11249  2clim  11264  climabs0  11270  climcn1  11271  climcn2  11272  climsqz  11298  climsqz2  11299  climub  11307  climserle  11308  fsum3cvg  11341  fisumss  11355  fsum3ser  11360  sumsplitdc  11395  fsump1i  11396  fsumlessfi  11423  telfsumo  11429  fsumparts  11433  iserabs  11438  binomlem  11446  isumsplit  11454  isum1p  11455  isumlessdc  11459  mertenslem2  11499  mertensabs  11500  prodfap0  11508  prodfrecap  11509  prodfdivap  11510  fproddccvg  11535  prodmodclem2  11540  fprodssdc  11553  fprodabs  11579  fprodeq0  11580  fprodeq0g  11601  ege2le3  11634  efsub  11644  efexp  11645  efsep  11654  sinsub  11703  cossub  11704  demoivre  11735  eirraplem  11739  moddvds  11761  0dvds  11773  iddvdsexp  11777  dvdssub  11800  dvdsle  11804  dvdsleabs  11805  dvdseq  11808  dvdsflip  11811  mulsucdiv2z  11844  divalgb  11884  divalg2  11885  ndvdsadd  11890  gcdneg  11937  gcdabs2  11945  modgcd  11946  bezoutlemsup  11964  gcdmultiplez  11976  gcdeq  11978  dvdssq  11986  lcmcllem  12021  lcmneg  12028  lcmdvds  12033  qredeu  12051  cncongrcoprm  12060  isprm3  12072  prmrp  12099  divnumden  12150  phiprmpw  12176  crth  12178  hashgcdlem  12192  hashgcdeq  12193  modprminv  12203  modprminveq  12204  modprmn0modprm0  12210  coprimeprodsq2  12212  pcpre1  12246  pccl  12253  pcmul  12255  pcdiv  12256  pcqcl  12260  pcexp  12263  pcdvds  12268  pcndvds  12270  pcndvds2  12272  pcelnn  12274  pcgcd1  12281  pc2dvds  12283  pc11  12284  gzsubcl  12332  4sqlem3  12342  setsresg  12454  submcl  12701  grpinvnzcl  12771  iunopn  12794  unopn  12797  eltg  12846  eltg2  12847  tgcl  12858  tgiun  12867  tgidm  12868  isopn3i  12929  isneip  12940  neipsm  12948  restbasg  12962  restopn2  12977  lmbrf  13009  cnclima  13017  lmss  13040  txbasval  13061  txlm  13073  psmetxrge0  13126  blininf  13218  blssps  13221  blss  13222  elmopn2  13243  bdmet  13296  metrest  13300  bl2ioo  13336  dvcjbr  13466  efper  13522  sinperlem  13523  abssinper  13561  cxpexprp  13610  logcxp  13612  rpcxpcl  13618  rpcxproot  13628  rprelogbmulexp  13668  lgsval2lem  13705  lgssq2  13736  lgsprme0  13737  bj-inex  13942  peano5set  13975  findset  13980  bj-findis  14014  nninfsellemsuc  14045  nninfself  14046  cvgcmp2nlemabs  14064  iooref1o  14066  trilpolemeq1  14072  nconstwlpolemgt0  14095