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  939  3adantr1  1158  3adantr2  1159  3adantr3  1160  syl3anr1  1301  syl3anr3  1303  dfbi3dc  1408  xordidc  1410  elabgt  2905  sbciegft  3020  csbtt  3096  csbnestgf  3137  copsex2t  4278  pofun  4347  onsucmin  4543  onsucelsucr  4544  onsucsssucr  4545  ordsucunielexmid  4567  ordsuc  4599  nlimsucg  4602  elnn  4642  xpsspw  4775  elxp4  5157  elxp5  5158  funimass2  5336  imain  5340  funimaexg  5342  f1ff1  5471  dff1o2  5509  resdif  5526  funbrfv  5599  fvelimab  5617  eqfnfv2  5660  fvimacnvi  5676  ffvresb  5725  fnressn  5748  fmptapd  5753  fnex  5784  rexima  5801  ralima  5802  f1elima  5820  fnotovb  5965  mpoeq12  5982  fovcdm  6066  fnovrn  6071  ofrfval  6144  ofvalg  6145  cofunexg  6166  cofunex2g  6167  mpoexxg  6268  mpoexg  6269  f1o2ndf1  6286  spc2ed  6291  smodm2  6353  tfrlem9  6377  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  tfri3  6425  rdgtfr  6432  rdgruledefgg  6433  oav2  6521  oasuc  6522  omv2  6523  onasuc  6524  omsuc  6530  onmsuc  6531  nnaass  6543  nndi  6544  nndir  6548  nnaword  6569  ecelqsg  6647  iinerm  6666  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  fvdiagfn  6752  ixpssmap2g  6786  domentr  6850  xpdom1g  6892  fopwdom  6897  ssenen  6912  phplem3  6915  phplem4  6916  php5dom  6924  ssfilem  6936  diffitest  6948  ctssdccl  7177  pm54.43  7257  addclpi  7394  addasspig  7397  mulasspig  7399  distrpig  7400  mulcanpig  7402  nnppipi  7410  enqdc1  7429  addassnqg  7449  ltbtwnnqq  7482  prarloclemarch  7485  prarloclemarch2  7486  enq0sym  7499  enq0ref  7500  addclnq0  7518  nqpnq0nq  7520  nnanq0  7525  distrnq0  7526  addassnq0lemcl  7528  addassnq0  7529  distnq0r  7530  prarloclemlt  7560  genpassl  7591  genpassu  7592  genpassg  7593  nqpru  7619  addcomprg  7645  mulcomprg  7647  distrlem1prl  7649  distrlem1pru  7650  1idprl  7657  1idpru  7658  recexprlemdisj  7697  recexprlem1ssl  7700  peano2nnnn  7920  ax1rid  7944  axcaucvglemcl  7962  le2tri3i  8135  add4  8187  cnegexlem1  8201  cnegexlem3  8203  cnegex  8204  subadd  8229  addsub  8237  addsubeq4  8241  negdi  8283  renegcl  8287  resubcl  8290  subdi  8411  mulneg2  8422  mul2neg  8424  submul2  8425  ltnegcon2  8491  lenegcon2  8494  lesub0  8506  cru  8629  recextlem1  8678  recexap  8680  div12ap  8721  divnegap  8733  letrp1  8875  dfinfre  8983  peano2nn  9002  nndivre  9026  nnsub  9029  nndivtr  9032  arch  9246  bndndx  9248  nn0addge1  9295  nn0addge2  9296  zaddcl  9366  zsubcl  9367  zltnle  9372  zrevaddcl  9376  nzadd  9378  zleltp1  9381  zltlem1  9383  zdiv  9414  peano2uz2  9433  uzind  9437  eluzp1l  9626  ublbneg  9687  qaddcl  9709  qsubcl  9712  qreccl  9716  qdivcl  9717  qrevaddcl  9718  irradd  9720  irrmul  9721  rerpdivcl  9759  nn0ledivnn  9842  xrre  9895  rexsub  9928  xaddass  9944  xnpcan  9947  xsubge0  9956  xposdif  9957  elioc2  10011  icoshft  10065  iccdil  10073  fzss2  10139  fzsuc2  10154  fzrev2  10160  elfzm11  10166  elfzp1b  10172  fzrevral  10180  fzshftral  10183  fzof  10219  fzoval  10223  fzon  10242  fzosubel  10270  zpnn0elfzo  10283  elfzom1b  10305  qltnle  10333  flqlt  10373  flqbi  10380  flqaddz  10387  fzofig  10524  seq3feq2  10568  ser3le  10629  expp1  10638  expm1t  10659  expeq0  10662  binom2sub  10745  bernneq  10752  expnlbnd  10756  zzlesq  10800  faccl  10827  facdiv  10830  bcpasc  10858  bccl  10859  ffz0hash  10925  fnfzo0hash  10927  wrdlen1  10972  wrdred1  10977  2shfti  10996  crim  11023  mulreap  11029  resub  11035  imsub  11043  ipcnval  11051  cjsub  11057  resqrexlemfp1  11174  resqrexlemgt0  11185  sqabsadd  11220  sqabssub  11221  abs2dif2  11272  cau3lem  11279  icodiamlt  11345  xrmaxaddlem  11425  clim  11446  clim2  11448  clim2c  11449  clim0c  11451  2clim  11466  climabs0  11472  climcn1  11473  climcn2  11474  climsqz  11500  climsqz2  11501  climub  11509  climserle  11510  fsum3cvg  11543  fisumss  11557  fsum3ser  11562  sumsplitdc  11597  fsump1i  11598  fsumlessfi  11625  telfsumo  11631  fsumparts  11635  iserabs  11640  binomlem  11648  isumsplit  11656  isum1p  11657  isumlessdc  11661  mertenslem2  11701  mertensabs  11702  prodfap0  11710  prodfrecap  11711  prodfdivap  11712  fproddccvg  11737  prodmodclem2  11742  fprodssdc  11755  fprodabs  11781  fprodeq0  11782  fprodeq0g  11803  ege2le3  11836  efsub  11846  efexp  11847  efsep  11856  sinsub  11905  cossub  11906  demoivre  11938  eirraplem  11942  moddvds  11964  0dvds  11976  iddvdsexp  11980  dvdssub  12003  dvdsle  12009  dvdsleabs  12010  dvdseq  12013  dvdsflip  12016  mulsucdiv2z  12050  divalgb  12090  divalg2  12091  ndvdsadd  12096  bitsp1  12115  gcdneg  12149  gcdabs2  12157  modgcd  12158  bezoutlemsup  12176  gcdmultiplez  12188  gcdeq  12190  dvdssq  12198  lcmcllem  12235  lcmneg  12242  lcmdvds  12247  qredeu  12265  cncongrcoprm  12274  isprm3  12286  prmrp  12313  divnumden  12364  phiprmpw  12390  crth  12392  hashgcdlem  12406  hashgcdeq  12408  modprminv  12418  modprminveq  12419  modprmn0modprm0  12425  coprimeprodsq2  12427  pcpre1  12461  pccl  12468  pcmul  12470  pcdiv  12471  pcqcl  12475  pcexp  12478  pcdvds  12484  pcndvds  12486  pcndvds2  12488  pcelnn  12490  pcgcd1  12497  pc2dvds  12499  pc11  12500  gzsubcl  12549  4sqlem3  12559  setsresg  12716  xpsfeq  12988  submcl  13111  grpinvnzcl  13204  mulgnnass  13287  nmzsubg  13340  nmznsg  13343  resghm2b  13392  ghmnsgpreima  13399  gsumfzsnfd  13475  iscrng2  13571  subrngpropd  13772  issubrg3  13803  subrgpropd  13809  islmodd  13849  lss1d  13939  lspsncl  13948  lspsnid  13963  df2idl2  14065  2idlcpbl  14080  qusrhm  14084  gsumfzfsumlemm  14143  iunopn  14238  unopn  14241  eltg  14288  eltg2  14289  tgcl  14300  tgiun  14309  tgidm  14310  isopn3i  14371  isneip  14382  neipsm  14390  restbasg  14404  restopn2  14419  lmbrf  14451  cnclima  14459  lmss  14482  txbasval  14503  txlm  14515  psmetxrge0  14568  blininf  14660  blssps  14663  blss  14664  elmopn2  14685  bdmet  14738  metrest  14742  bl2ioo  14786  dvcjbr  14944  plyaddlem1  14983  plymullem1  14984  plyreres  15000  dvply1  15001  dvply2g  15002  efper  15043  sinperlem  15044  abssinper  15082  cxpexprp  15131  logcxp  15133  rpcxpcl  15139  rpcxproot  15150  rprelogbmulexp  15192  lgsval2lem  15251  lgssq2  15282  lgsprme0  15283  bj-inex  15553  peano5set  15586  findset  15591  bj-findis  15625  nninfsellemsuc  15656  nninfself  15657  cvgcmp2nlemabs  15676  iooref1o  15678  trilpolemeq1  15684  nconstwlpolemgt0  15708