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  2948  sbciegft  3063  csbtt  3140  csbnestgf  3181  copsex2t  4343  pofun  4415  onsucmin  4611  onsucelsucr  4612  onsucsssucr  4613  ordsucunielexmid  4635  ordsuc  4667  nlimsucg  4670  elnn  4710  xpsspw  4844  elxp4  5231  elxp5  5232  funimass2  5415  imain  5419  funimaexg  5421  f1ff1  5559  dff1o2  5597  resdif  5614  funbrfv  5691  fnbrfvb2  5697  fvelimab  5711  eqfnfv2  5754  fvimacnvi  5770  ffvresb  5818  fnressn  5848  fmptapd  5853  fnex  5884  rexima  5905  ralima  5906  f1elima  5924  fnotovb  6074  mpoeq12  6091  fovcdm  6175  fnovrn  6180  ofrfval  6253  ofvalg  6254  cofunexg  6280  cofunex2g  6281  mpoexxg  6384  mpoexg  6385  f1o2ndf1  6402  spc2ed  6407  funsssuppss  6436  smodm2  6504  tfrlem9  6528  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  tfri3  6576  rdgtfr  6583  rdgruledefgg  6584  oav2  6674  oasuc  6675  omv2  6676  onasuc  6677  omsuc  6683  onmsuc  6684  nnaass  6696  nndi  6697  nndir  6701  nnaword  6722  ecelqsg  6800  iinerm  6819  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  fvdiagfn  6905  ixpssmap2g  6939  domentr  7008  xpdom1g  7060  fopwdom  7065  ssenen  7080  phplem3  7083  phplem4  7084  php5dom  7092  ssfilem  7105  ssfilemd  7107  diffitest  7119  ctssdccl  7353  pm54.43  7438  pw1if  7486  addclpi  7590  addasspig  7593  mulasspig  7595  distrpig  7596  mulcanpig  7598  nnppipi  7606  enqdc1  7625  addassnqg  7645  ltbtwnnqq  7678  prarloclemarch  7681  prarloclemarch2  7682  enq0sym  7695  enq0ref  7696  addclnq0  7714  nqpnq0nq  7716  nnanq0  7721  distrnq0  7722  addassnq0lemcl  7724  addassnq0  7725  distnq0r  7726  prarloclemlt  7756  genpassl  7787  genpassu  7788  genpassg  7789  nqpru  7815  addcomprg  7841  mulcomprg  7843  distrlem1prl  7845  distrlem1pru  7846  1idprl  7853  1idpru  7854  recexprlemdisj  7893  recexprlem1ssl  7896  peano2nnnn  8116  ax1rid  8140  axcaucvglemcl  8158  le2tri3i  8330  add4  8382  cnegexlem1  8396  cnegexlem3  8398  cnegex  8399  subadd  8424  addsub  8432  addsubeq4  8436  negdi  8478  renegcl  8482  resubcl  8485  subdi  8606  mulneg2  8617  mul2neg  8619  submul2  8620  ltnegcon2  8686  lenegcon2  8689  lesub0  8701  cru  8824  recextlem1  8873  recexap  8875  div12ap  8916  divnegap  8928  letrp1  9070  dfinfre  9178  peano2nn  9197  nndivre  9221  nnsub  9224  nndivtr  9227  arch  9441  bndndx  9443  nn0addge1  9490  nn0addge2  9491  zaddcl  9563  zsubcl  9564  zltnle  9569  zrevaddcl  9574  nzadd  9576  zleltp1  9579  zltlem1  9581  zdiv  9612  peano2uz2  9631  uzind  9635  eluzp1l  9825  ublbneg  9891  qaddcl  9913  qsubcl  9916  qreccl  9920  qdivcl  9921  qrevaddcl  9922  irradd  9924  irrmul  9925  rerpdivcl  9963  nn0ledivnn  10046  xrre  10099  rexsub  10132  xaddass  10148  xnpcan  10151  xsubge0  10160  xposdif  10161  elioc2  10215  icoshft  10269  iccdil  10277  fzss2  10344  fzsuc2  10359  fzrev2  10365  elfzm11  10371  elfzp1b  10377  fzrevral  10385  fzshftral  10388  fzof  10424  fzoval  10428  fzon  10447  elfzoextl  10482  fzosubel  10485  zpnn0elfzo  10498  elfzom1b  10520  qltnle  10549  flqlt  10589  flqbi  10596  flqaddz  10603  fzofig  10740  seq3feq2  10784  ser3le  10845  expp1  10854  expm1t  10875  expeq0  10878  binom2sub  10961  bernneq  10968  expnlbnd  10972  zzlesq  11016  faccl  11043  facdiv  11046  bcpasc  11074  bccl  11075  ffz0hash  11143  fnfzo0hash  11145  wrdlen1  11200  wrdred1  11205  ccatval21sw  11231  wrdl1exs1  11255  ccatws1cl  11258  ccatws1leng  11260  pfxmpt  11310  pfxfv  11314  pfxfvlsw  11325  ccatpfx  11331  pfx1  11333  swrdccatin1  11355  swrdccat  11365  pfxccatpfx1  11366  2shfti  11454  crim  11481  mulreap  11487  resub  11493  imsub  11501  ipcnval  11509  cjsub  11515  resqrexlemfp1  11632  resqrexlemgt0  11643  sqabsadd  11678  sqabssub  11679  abs2dif2  11730  cau3lem  11737  icodiamlt  11803  xrmaxaddlem  11883  clim  11904  clim2  11906  clim2c  11907  clim0c  11909  2clim  11924  climabs0  11930  climcn1  11931  climcn2  11932  climsqz  11958  climsqz2  11959  climub  11967  climserle  11968  fsum3cvg  12002  fisumss  12016  fsum3ser  12021  sumsplitdc  12056  fsump1i  12057  fsumlessfi  12084  telfsumo  12090  fsumparts  12094  iserabs  12099  binomlem  12107  isumsplit  12115  isum1p  12116  isumlessdc  12120  mertenslem2  12160  mertensabs  12161  prodfap0  12169  prodfrecap  12170  prodfdivap  12171  fproddccvg  12196  prodmodclem2  12201  fprodssdc  12214  fprodabs  12240  fprodeq0  12241  fprodeq0g  12262  ege2le3  12295  efsub  12305  efexp  12306  efsep  12315  sinsub  12364  cossub  12365  demoivre  12397  eirraplem  12401  moddvds  12423  0dvds  12435  iddvdsexp  12439  dvdssub  12462  dvdsle  12468  dvdsleabs  12469  dvdseq  12472  dvdsflip  12475  mulsucdiv2z  12509  divalgb  12549  divalg2  12550  ndvdsadd  12555  bitsp1  12575  gcdneg  12616  gcdabs2  12624  modgcd  12625  bezoutlemsup  12643  gcdmultiplez  12655  gcdeq  12657  dvdssq  12665  lcmcllem  12702  lcmneg  12709  lcmdvds  12714  qredeu  12732  cncongrcoprm  12741  isprm3  12753  prmrp  12780  divnumden  12831  phiprmpw  12857  crth  12859  hashgcdlem  12873  hashgcdeq  12875  modprminv  12885  modprminveq  12886  modprmn0modprm0  12892  coprimeprodsq2  12894  pcpre1  12928  pccl  12935  pcmul  12937  pcdiv  12938  pcqcl  12942  pcexp  12945  pcdvds  12951  pcndvds  12953  pcndvds2  12955  pcelnn  12957  pcgcd1  12964  pc2dvds  12966  pc11  12967  gzsubcl  13016  4sqlem3  13026  setsresg  13183  pwssnf1o  13444  xpsfeq  13491  submcl  13625  grpinvnzcl  13718  mulgnnass  13807  nmzsubg  13860  nmznsg  13863  resghm2b  13912  ghmnsgpreima  13919  gsumfzsnfd  13995  iscrng2  14092  subrngpropd  14294  issubrg3  14325  subrgpropd  14331  islmodd  14372  lss1d  14462  lspsncl  14471  lspsnid  14486  df2idl2  14588  2idlcpbl  14603  qusrhm  14607  gsumfzfsumlemm  14666  iunopn  14796  unopn  14799  eltg  14846  eltg2  14847  tgcl  14858  tgiun  14867  tgidm  14868  isopn3i  14929  isneip  14940  neipsm  14948  restbasg  14962  restopn2  14977  lmbrf  15009  cnclima  15017  lmss  15040  txbasval  15061  txlm  15073  psmetxrge0  15126  blininf  15218  blssps  15221  blss  15222  elmopn2  15243  bdmet  15296  metrest  15300  bl2ioo  15344  dvcjbr  15502  plyaddlem1  15541  plymullem1  15542  plyreres  15558  dvply1  15559  dvply2g  15560  efper  15601  sinperlem  15602  abssinper  15640  cxpexprp  15689  logcxp  15691  rpcxpcl  15697  rpcxproot  15708  rprelogbmulexp  15750  lgsval2lem  15812  lgssq2  15843  lgsprme0  15844  ausgrusgrben  16092  wlkepvtx  16299  bj-inex  16606  peano5set  16639  findset  16644  bj-findis  16678  nninfsellemsuc  16721  nninfself  16722  cvgcmp2nlemabs  16747  iooref1o  16749  trilpolemeq1  16755  nconstwlpolemgt0  16780