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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  408  sylanr2  409  mpanr2  442  adantrl  482  adantrr  483  ancom2s  572  annimdc  950  ifpnst  1001  3adantr1  1187  3adantr2  1188  3adantr3  1189  syl3anr1  1330  syl3anr3  1332  dfbi3dc  1446  xordidc  1448  elabgt  2967  sbciegft  3082  csbtt  3159  csbnestgf  3200  copsex2t  4385  pofun  4457  onsucmin  4654  onsucelsucr  4655  onsucsssucr  4656  ordsucunielexmid  4678  ordsuc  4710  nlimsucg  4713  elnn  4753  xpsspw  4887  elxp4  5275  elxp5  5276  funimass2  5459  imain  5463  funimaexg  5465  f1ff1  5606  dff1o2  5644  resdif  5661  funbrfv  5739  fnbrfvb2  5745  fvelimab  5759  eqfnfv2  5807  fvimacnvi  5823  ffvresb  5871  fnressn  5901  fmptapd  5906  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fnotovb  6131  mpoeq12  6148  fovcdm  6232  fnovrn  6237  ofrfval  6311  ofvalg  6312  cofunexg  6338  cofunex2g  6339  mpoexxg  6446  mpoexg  6447  f1o2ndf1  6464  spc2ed  6469  funsssuppss  6498  smodm2  6566  tfrlem9  6590  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  oav2  6736  oasuc  6737  omv2  6738  onasuc  6739  omsuc  6745  onmsuc  6746  nnaass  6758  nndi  6759  nndir  6763  nnaword  6784  ecelqsg  6862  iinerm  6881  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  fvdiagfn  6975  ixpssmap2g  7009  domentr  7078  xpdom1g  7131  fopwdom  7136  ssenen  7152  phplem3  7155  phplem4  7156  php5dom  7164  ssfilem  7177  ssfilemd  7179  diffitest  7191  ctssdccl  7451  pm54.43  7536  pw1if  7584  addclpi  7694  addasspig  7697  mulasspig  7699  distrpig  7700  mulcanpig  7702  nnppipi  7710  enqdc1  7729  addassnqg  7749  ltbtwnnqq  7782  prarloclemarch  7785  prarloclemarch2  7786  enq0sym  7799  enq0ref  7800  addclnq0  7818  nqpnq0nq  7820  nnanq0  7825  distrnq0  7826  addassnq0lemcl  7828  addassnq0  7829  distnq0r  7830  prarloclemlt  7860  genpassl  7891  genpassu  7892  genpassg  7893  nqpru  7919  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  1idprl  7957  1idpru  7958  recexprlemdisj  7997  recexprlem1ssl  8000  peano2nnnn  8220  ax1rid  8244  axcaucvglemcl  8262  le2tri3i  8434  add4  8487  cnegexlem1  8501  cnegexlem3  8503  cnegex  8504  subadd  8529  addsub  8537  addsubeq4  8541  negdi  8583  renegcl  8587  resubcl  8590  subdi  8712  mulneg2  8723  mul2neg  8725  submul2  8726  ltnegcon2  8792  lenegcon2  8795  lesub0  8807  cru  8930  recextlem1  8979  recexap  8981  div12ap  9024  divnegap  9036  letrp1  9178  dfinfre  9286  peano2nn  9316  nndivre  9340  nnsub  9343  nndivtr  9346  arch  9560  bndndx  9562  nn0addge1  9609  nn0addge2  9610  zaddcl  9684  zsubcl  9685  zltnle  9690  zrevaddcl  9695  nzadd  9697  zleltp1  9700  zltlem1  9702  zdiv  9734  peano2uz2  9753  uzind  9757  eluzp1l  9947  ublbneg  10013  qaddcl  10035  qsubcl  10038  qreccl  10042  qdivcl  10043  qrevaddcl  10044  irradd  10046  irrmul  10047  rerpdivcl  10085  nn0ledivnn  10168  xrre  10222  rexsub  10255  xaddass  10271  xnpcan  10274  xsubge0  10283  xposdif  10284  elioc2  10338  icoshft  10392  iccdil  10400  fzss2  10470  fzsuc2  10486  fzrev2  10492  elfzm11  10498  elfzp1b  10504  fzrevral  10512  fzshftral  10515  fzof  10551  fzoval  10555  fzon  10574  elfzoextl  10609  fzosubel  10612  zpnn0elfzo  10625  elfzom1b  10647  qltnle  10678  flqlt  10718  flqbi  10725  flqaddz  10732  fzofig  10869  seq3feq2  10913  ser3le  10974  expp1  10983  expm1t  11004  expeq0  11007  binom2sub  11090  bernneq  11098  expnlbnd  11102  zzlesq  11146  faccl  11173  facdiv  11176  bcpasc  11204  bccl  11205  ffz0hash  11276  fnfzo0hash  11278  hashfibclem  11282  hashf1lem2  11286  wrdlen1  11342  wrdred1  11347  ccatval21sw  11373  wrdl1exs1  11397  ccatws1cl  11400  ccatws1leng  11402  pfxmpt  11452  pfxfv  11456  pfxfvlsw  11467  ccatpfx  11473  pfx1  11475  swrdccatin1  11497  swrdccat  11507  pfxccatpfx1  11508  2shfti  11596  crim  11623  mulreap  11629  resub  11635  imsub  11643  ipcnval  11651  cjsub  11657  resqrexlemfp1  11775  resqrexlemgt0  11786  sqabsadd  11821  sqabssub  11822  abs2dif2  11873  cau3lem  11880  icodiamlt  11946  xrmaxaddlem  12026  clim  12047  clim2  12049  clim2c  12050  clim0c  12052  2clim  12067  climabs0  12073  climcn1  12074  climcn2  12075  climsqz  12101  climsqz2  12102  climub  12110  climserle  12111  fsum3cvg  12145  fisumss  12159  fsum3ser  12164  sumsplitdc  12199  fsump1i  12200  fsumlessfi  12227  telfsumo  12233  fsumparts  12237  iserabs  12242  binomlem  12250  isumsplit  12258  isum1p  12259  isumlessdc  12263  mertenslem2  12303  mertensabs  12304  prodfap0  12312  prodfrecap  12313  prodfdivap  12314  fproddccvg  12339  prodmodclem2  12344  fprodssdc  12357  fprodabs  12383  fprodeq0  12384  fprodeq0g  12405  ege2le3  12438  efsub  12448  efexp  12449  efsep  12458  sinsub  12507  cossub  12508  demoivre  12540  eirraplem  12544  moddvds  12566  0dvds  12578  iddvdsexp  12582  dvdssub  12605  dvdsle  12611  dvdsleabs  12612  dvdseq  12615  dvdsflip  12618  mulsucdiv2z  12652  divalgb  12692  divalg2  12693  ndvdsadd  12698  bitsp1  12718  gcdneg  12759  gcdabs2  12767  modgcd  12768  bezoutlemsup  12786  gcdmultiplez  12798  gcdeq  12800  dvdssq  12808  lcmcllem  12845  lcmneg  12852  lcmdvds  12857  qredeu  12875  cncongrcoprm  12884  isprm3  12896  prmrp  12923  divnumden  12974  phiprmpw  13000  crth  13002  hashgcdlem  13016  hashgcdeq  13018  modprminv  13028  modprminveq  13029  modprmn0modprm0  13035  coprimeprodsq2  13037  pcpre1  13071  pccl  13078  pcmul  13080  pcdiv  13081  pcqcl  13085  pcexp  13088  pcdvds  13094  pcndvds  13096  pcndvds2  13098  pcelnn  13100  pcgcd1  13107  pc2dvds  13109  pc11  13110  gzsubcl  13159  4sqlem3  13169  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  ballotfilemfrceq  13272  setsresg  13390  xpsfeq  13666  submcl  13786  grpinvnzcl  13877  mulgnnass  13960  nmzsubg  14013  nmznsg  14016  resghm2b  14065  ghmnsgpreima  14072  gzsumsnfd  14147  pwssnf1o  14211  iscrng2  14319  subrngpropd  14524  issubrg3  14555  subrgpropd  14561  islmodd  14629  lss1d  14720  lspsncl  14729  lspsnid  14744  df2idl2  14846  2idlcpbl  14861  qusrhm  14865  iunopn  15103  unopn  15106  eltg  15153  eltg2  15154  tgcl  15165  tgiun  15174  tgidm  15175  isopn3i  15236  isneip  15247  neipsm  15255  restbasg  15269  restopn2  15284  lmbrf  15316  cnclima  15324  lmss  15347  txbasval  15368  txlm  15380  psmetxrge0  15433  blininf  15525  blssps  15528  blss  15529  elmopn2  15550  bdmet  15603  metrest  15607  bl2ioo  15651  dvcjbr  15809  plyaddlem1  15848  plymullem1  15849  plyreres  15865  dvply1  15866  dvply2g  15867  efper  15908  sinperlem  15909  abssinper  15947  cxpexprp  15997  logcxp  15999  rpcxpcl  16005  rpcxproot  16016  rprelogbmulexp  16058  log2tlbndlog2  16082  lgsval2lem  16129  lgssq2  16160  lgsprme0  16161  ausgrusgrben  16409  wlkepvtx  16616  bj-inex  16933  peano5set  16966  findset  16971  bj-findis  17005  nninfsellemsuc  17055  nninfself  17056  cvgcmp2nlemabs  17081  iooref1o  17083  trilpolemeq1  17089  nconstwlpolemgt0  17114