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  943  ifpnst  994  3adantr1  1180  3adantr2  1181  3adantr3  1182  syl3anr1  1323  syl3anr3  1325  dfbi3dc  1439  xordidc  1441  elabgt  2944  sbciegft  3059  csbtt  3136  csbnestgf  3177  copsex2t  4330  pofun  4402  onsucmin  4598  onsucelsucr  4599  onsucsssucr  4600  ordsucunielexmid  4622  ordsuc  4654  nlimsucg  4657  elnn  4697  xpsspw  4830  elxp4  5215  elxp5  5216  funimass2  5398  imain  5402  funimaexg  5404  f1ff1  5538  dff1o2  5576  resdif  5593  funbrfv  5669  fnbrfvb2  5675  fvelimab  5689  eqfnfv2  5732  fvimacnvi  5748  ffvresb  5797  fnressn  5824  fmptapd  5829  fnex  5860  rexima  5877  ralima  5878  f1elima  5896  fnotovb  6046  mpoeq12  6063  fovcdm  6147  fnovrn  6152  ofrfval  6225  ofvalg  6226  cofunexg  6252  cofunex2g  6253  mpoexxg  6354  mpoexg  6355  f1o2ndf1  6372  spc2ed  6377  smodm2  6439  tfrlem9  6463  tfrlemibxssdm  6471  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  tfri3  6511  rdgtfr  6518  rdgruledefgg  6519  oav2  6607  oasuc  6608  omv2  6609  onasuc  6610  omsuc  6616  onmsuc  6617  nnaass  6629  nndi  6630  nndir  6634  nnaword  6655  ecelqsg  6733  iinerm  6752  ecovass  6789  ecoviass  6790  ecovdi  6791  ecovidi  6792  fvdiagfn  6838  ixpssmap2g  6872  domentr  6941  xpdom1g  6988  fopwdom  6993  ssenen  7008  phplem3  7011  phplem4  7012  php5dom  7020  ssfilem  7033  diffitest  7045  ctssdccl  7274  pm54.43  7359  pw1if  7406  addclpi  7510  addasspig  7513  mulasspig  7515  distrpig  7516  mulcanpig  7518  nnppipi  7526  enqdc1  7545  addassnqg  7565  ltbtwnnqq  7598  prarloclemarch  7601  prarloclemarch2  7602  enq0sym  7615  enq0ref  7616  addclnq0  7634  nqpnq0nq  7636  nnanq0  7641  distrnq0  7642  addassnq0lemcl  7644  addassnq0  7645  distnq0r  7646  prarloclemlt  7676  genpassl  7707  genpassu  7708  genpassg  7709  nqpru  7735  addcomprg  7761  mulcomprg  7763  distrlem1prl  7765  distrlem1pru  7766  1idprl  7773  1idpru  7774  recexprlemdisj  7813  recexprlem1ssl  7816  peano2nnnn  8036  ax1rid  8060  axcaucvglemcl  8078  le2tri3i  8251  add4  8303  cnegexlem1  8317  cnegexlem3  8319  cnegex  8320  subadd  8345  addsub  8353  addsubeq4  8357  negdi  8399  renegcl  8403  resubcl  8406  subdi  8527  mulneg2  8538  mul2neg  8540  submul2  8541  ltnegcon2  8607  lenegcon2  8610  lesub0  8622  cru  8745  recextlem1  8794  recexap  8796  div12ap  8837  divnegap  8849  letrp1  8991  dfinfre  9099  peano2nn  9118  nndivre  9142  nnsub  9145  nndivtr  9148  arch  9362  bndndx  9364  nn0addge1  9411  nn0addge2  9412  zaddcl  9482  zsubcl  9483  zltnle  9488  zrevaddcl  9493  nzadd  9495  zleltp1  9498  zltlem1  9500  zdiv  9531  peano2uz2  9550  uzind  9554  eluzp1l  9743  ublbneg  9804  qaddcl  9826  qsubcl  9829  qreccl  9833  qdivcl  9834  qrevaddcl  9835  irradd  9837  irrmul  9838  rerpdivcl  9876  nn0ledivnn  9959  xrre  10012  rexsub  10045  xaddass  10061  xnpcan  10064  xsubge0  10073  xposdif  10074  elioc2  10128  icoshft  10182  iccdil  10190  fzss2  10256  fzsuc2  10271  fzrev2  10277  elfzm11  10283  elfzp1b  10289  fzrevral  10297  fzshftral  10300  fzof  10336  fzoval  10340  fzon  10359  elfzoextl  10392  fzosubel  10395  zpnn0elfzo  10408  elfzom1b  10430  qltnle  10458  flqlt  10498  flqbi  10505  flqaddz  10512  fzofig  10649  seq3feq2  10693  ser3le  10754  expp1  10763  expm1t  10784  expeq0  10787  binom2sub  10870  bernneq  10877  expnlbnd  10881  zzlesq  10925  faccl  10952  facdiv  10955  bcpasc  10983  bccl  10984  ffz0hash  11050  fnfzo0hash  11052  wrdlen1  11104  wrdred1  11109  ccatval21sw  11135  wrdl1exs1  11157  ccatws1cl  11160  ccatws1leng  11162  pfxmpt  11207  pfxfv  11211  pfxfvlsw  11222  ccatpfx  11228  pfx1  11230  swrdccatin1  11252  swrdccat  11262  pfxccatpfx1  11263  2shfti  11337  crim  11364  mulreap  11370  resub  11376  imsub  11384  ipcnval  11392  cjsub  11398  resqrexlemfp1  11515  resqrexlemgt0  11526  sqabsadd  11561  sqabssub  11562  abs2dif2  11613  cau3lem  11620  icodiamlt  11686  xrmaxaddlem  11766  clim  11787  clim2  11789  clim2c  11790  clim0c  11792  2clim  11807  climabs0  11813  climcn1  11814  climcn2  11815  climsqz  11841  climsqz2  11842  climub  11850  climserle  11851  fsum3cvg  11884  fisumss  11898  fsum3ser  11903  sumsplitdc  11938  fsump1i  11939  fsumlessfi  11966  telfsumo  11972  fsumparts  11976  iserabs  11981  binomlem  11989  isumsplit  11997  isum1p  11998  isumlessdc  12002  mertenslem2  12042  mertensabs  12043  prodfap0  12051  prodfrecap  12052  prodfdivap  12053  fproddccvg  12078  prodmodclem2  12083  fprodssdc  12096  fprodabs  12122  fprodeq0  12123  fprodeq0g  12144  ege2le3  12177  efsub  12187  efexp  12188  efsep  12197  sinsub  12246  cossub  12247  demoivre  12279  eirraplem  12283  moddvds  12305  0dvds  12317  iddvdsexp  12321  dvdssub  12344  dvdsle  12350  dvdsleabs  12351  dvdseq  12354  dvdsflip  12357  mulsucdiv2z  12391  divalgb  12431  divalg2  12432  ndvdsadd  12437  bitsp1  12457  gcdneg  12498  gcdabs2  12506  modgcd  12507  bezoutlemsup  12525  gcdmultiplez  12537  gcdeq  12539  dvdssq  12547  lcmcllem  12584  lcmneg  12591  lcmdvds  12596  qredeu  12614  cncongrcoprm  12623  isprm3  12635  prmrp  12662  divnumden  12713  phiprmpw  12739  crth  12741  hashgcdlem  12755  hashgcdeq  12757  modprminv  12767  modprminveq  12768  modprmn0modprm0  12774  coprimeprodsq2  12776  pcpre1  12810  pccl  12817  pcmul  12819  pcdiv  12820  pcqcl  12824  pcexp  12827  pcdvds  12833  pcndvds  12835  pcndvds2  12837  pcelnn  12839  pcgcd1  12846  pc2dvds  12848  pc11  12849  gzsubcl  12898  4sqlem3  12908  setsresg  13065  pwssnf1o  13326  xpsfeq  13373  submcl  13507  grpinvnzcl  13600  mulgnnass  13689  nmzsubg  13742  nmznsg  13745  resghm2b  13794  ghmnsgpreima  13801  gsumfzsnfd  13877  iscrng2  13973  subrngpropd  14174  issubrg3  14205  subrgpropd  14211  islmodd  14251  lss1d  14341  lspsncl  14350  lspsnid  14365  df2idl2  14467  2idlcpbl  14482  qusrhm  14486  gsumfzfsumlemm  14545  iunopn  14670  unopn  14673  eltg  14720  eltg2  14721  tgcl  14732  tgiun  14741  tgidm  14742  isopn3i  14803  isneip  14814  neipsm  14822  restbasg  14836  restopn2  14851  lmbrf  14883  cnclima  14891  lmss  14914  txbasval  14935  txlm  14947  psmetxrge0  15000  blininf  15092  blssps  15095  blss  15096  elmopn2  15117  bdmet  15170  metrest  15174  bl2ioo  15218  dvcjbr  15376  plyaddlem1  15415  plymullem1  15416  plyreres  15432  dvply1  15433  dvply2g  15434  efper  15475  sinperlem  15476  abssinper  15514  cxpexprp  15563  logcxp  15565  rpcxpcl  15571  rpcxproot  15582  rprelogbmulexp  15624  lgsval2lem  15683  lgssq2  15714  lgsprme0  15715  ausgrusgrben  15960  bj-inex  16228  peano5set  16261  findset  16266  bj-findis  16300  nninfsellemsuc  16337  nninfself  16338  cvgcmp2nlemabs  16359  iooref1o  16361  trilpolemeq1  16367  nconstwlpolemgt0  16391