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  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  4380  pofun  4452  onsucmin  4649  onsucelsucr  4650  onsucsssucr  4651  ordsucunielexmid  4673  ordsuc  4705  nlimsucg  4708  elnn  4748  xpsspw  4882  elxp4  5270  elxp5  5271  funimass2  5454  imain  5458  funimaexg  5460  f1ff1  5601  dff1o2  5639  resdif  5656  funbrfv  5733  fnbrfvb2  5739  fvelimab  5753  eqfnfv2  5798  fvimacnvi  5814  ffvresb  5862  fnressn  5892  fmptapd  5897  fnex  5928  rexima  5950  ralima  5951  f1elima  5969  fnotovb  6121  mpoeq12  6138  fovcdm  6222  fnovrn  6227  ofrfval  6301  ofvalg  6302  cofunexg  6328  cofunex2g  6329  mpoexxg  6436  mpoexg  6437  f1o2ndf1  6454  spc2ed  6459  funsssuppss  6488  smodm2  6556  tfrlem9  6580  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  tfri3  6628  rdgtfr  6635  rdgruledefgg  6636  oav2  6726  oasuc  6727  omv2  6728  onasuc  6729  omsuc  6735  onmsuc  6736  nnaass  6748  nndi  6749  nndir  6753  nnaword  6774  ecelqsg  6852  iinerm  6871  ecovass  6908  ecoviass  6909  ecovdi  6910  ecovidi  6911  fvdiagfn  6965  ixpssmap2g  6999  domentr  7068  xpdom1g  7121  fopwdom  7126  ssenen  7142  phplem3  7145  phplem4  7146  php5dom  7154  ssfilem  7167  ssfilemd  7169  diffitest  7181  ctssdccl  7441  pm54.43  7526  pw1if  7574  addclpi  7684  addasspig  7687  mulasspig  7689  distrpig  7690  mulcanpig  7692  nnppipi  7700  enqdc1  7719  addassnqg  7739  ltbtwnnqq  7772  prarloclemarch  7775  prarloclemarch2  7776  enq0sym  7789  enq0ref  7790  addclnq0  7808  nqpnq0nq  7810  nnanq0  7815  distrnq0  7816  addassnq0lemcl  7818  addassnq0  7819  distnq0r  7820  prarloclemlt  7850  genpassl  7881  genpassu  7882  genpassg  7883  nqpru  7909  addcomprg  7935  mulcomprg  7937  distrlem1prl  7939  distrlem1pru  7940  1idprl  7947  1idpru  7948  recexprlemdisj  7987  recexprlem1ssl  7990  peano2nnnn  8210  ax1rid  8234  axcaucvglemcl  8252  le2tri3i  8424  add4  8477  cnegexlem1  8491  cnegexlem3  8493  cnegex  8494  subadd  8519  addsub  8527  addsubeq4  8531  negdi  8573  renegcl  8577  resubcl  8580  subdi  8702  mulneg2  8713  mul2neg  8715  submul2  8716  ltnegcon2  8782  lenegcon2  8785  lesub0  8797  cru  8920  recextlem1  8969  recexap  8971  div12ap  9014  divnegap  9026  letrp1  9168  dfinfre  9276  peano2nn  9295  nndivre  9319  nnsub  9322  nndivtr  9325  arch  9539  bndndx  9541  nn0addge1  9588  nn0addge2  9589  zaddcl  9663  zsubcl  9664  zltnle  9669  zrevaddcl  9674  nzadd  9676  zleltp1  9679  zltlem1  9681  zdiv  9713  peano2uz2  9732  uzind  9736  eluzp1l  9926  ublbneg  9992  qaddcl  10014  qsubcl  10017  qreccl  10021  qdivcl  10022  qrevaddcl  10023  irradd  10025  irrmul  10026  rerpdivcl  10064  nn0ledivnn  10147  xrre  10201  rexsub  10234  xaddass  10250  xnpcan  10253  xsubge0  10262  xposdif  10263  elioc2  10317  icoshft  10371  iccdil  10379  fzss2  10448  fzsuc2  10464  fzrev2  10470  elfzm11  10476  elfzp1b  10482  fzrevral  10490  fzshftral  10493  fzof  10529  fzoval  10533  fzon  10552  elfzoextl  10587  fzosubel  10590  zpnn0elfzo  10603  elfzom1b  10625  qltnle  10656  flqlt  10696  flqbi  10703  flqaddz  10710  fzofig  10847  seq3feq2  10891  ser3le  10952  expp1  10961  expm1t  10982  expeq0  10985  binom2sub  11068  bernneq  11076  expnlbnd  11080  zzlesq  11124  faccl  11151  facdiv  11154  bcpasc  11182  bccl  11183  ffz0hash  11254  fnfzo0hash  11256  hashfibclem  11260  hashf1lem2  11264  wrdlen1  11320  wrdred1  11325  ccatval21sw  11351  wrdl1exs1  11375  ccatws1cl  11378  ccatws1leng  11380  pfxmpt  11430  pfxfv  11434  pfxfvlsw  11445  ccatpfx  11451  pfx1  11453  swrdccatin1  11475  swrdccat  11485  pfxccatpfx1  11486  2shfti  11574  crim  11601  mulreap  11607  resub  11613  imsub  11621  ipcnval  11629  cjsub  11635  resqrexlemfp1  11753  resqrexlemgt0  11764  sqabsadd  11799  sqabssub  11800  abs2dif2  11851  cau3lem  11858  icodiamlt  11924  xrmaxaddlem  12004  clim  12025  clim2  12027  clim2c  12028  clim0c  12030  2clim  12045  climabs0  12051  climcn1  12052  climcn2  12053  climsqz  12079  climsqz2  12080  climub  12088  climserle  12089  fsum3cvg  12123  fisumss  12137  fsum3ser  12142  sumsplitdc  12177  fsump1i  12178  fsumlessfi  12205  telfsumo  12211  fsumparts  12215  iserabs  12220  binomlem  12228  isumsplit  12236  isum1p  12237  isumlessdc  12241  mertenslem2  12281  mertensabs  12282  prodfap0  12290  prodfrecap  12291  prodfdivap  12292  fproddccvg  12317  prodmodclem2  12322  fprodssdc  12335  fprodabs  12361  fprodeq0  12362  fprodeq0g  12383  ege2le3  12416  efsub  12426  efexp  12427  efsep  12436  sinsub  12485  cossub  12486  demoivre  12518  eirraplem  12522  moddvds  12544  0dvds  12556  iddvdsexp  12560  dvdssub  12583  dvdsle  12589  dvdsleabs  12590  dvdseq  12593  dvdsflip  12596  mulsucdiv2z  12630  divalgb  12670  divalg2  12671  ndvdsadd  12676  bitsp1  12696  gcdneg  12737  gcdabs2  12745  modgcd  12746  bezoutlemsup  12764  gcdmultiplez  12776  gcdeq  12778  dvdssq  12786  lcmcllem  12823  lcmneg  12830  lcmdvds  12835  qredeu  12853  cncongrcoprm  12862  isprm3  12874  prmrp  12901  divnumden  12952  phiprmpw  12978  crth  12980  hashgcdlem  12994  hashgcdeq  12996  modprminv  13006  modprminveq  13007  modprmn0modprm0  13013  coprimeprodsq2  13015  pcpre1  13049  pccl  13056  pcmul  13058  pcdiv  13059  pcqcl  13063  pcexp  13066  pcdvds  13072  pcndvds  13074  pcndvds2  13076  pcelnn  13078  pcgcd1  13085  pc2dvds  13087  pc11  13088  gzsubcl  13137  4sqlem3  13147  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  ballotfilemfrceq  13250  setsresg  13368  xpsfeq  13643  submcl  13763  grpinvnzcl  13854  mulgnnass  13937  nmzsubg  13990  nmznsg  13993  resghm2b  14042  ghmnsgpreima  14049  gzsumsnfd  14124  pwssnf1o  14188  iscrng2  14293  subrngpropd  14497  issubrg3  14528  subrgpropd  14534  islmodd  14602  lss1d  14692  lspsncl  14701  lspsnid  14716  df2idl2  14818  2idlcpbl  14833  qusrhm  14837  iunopn  15026  unopn  15029  eltg  15076  eltg2  15077  tgcl  15088  tgiun  15097  tgidm  15098  isopn3i  15159  isneip  15170  neipsm  15178  restbasg  15192  restopn2  15207  lmbrf  15239  cnclima  15247  lmss  15270  txbasval  15291  txlm  15303  psmetxrge0  15356  blininf  15448  blssps  15451  blss  15452  elmopn2  15473  bdmet  15526  metrest  15530  bl2ioo  15574  dvcjbr  15732  plyaddlem1  15771  plymullem1  15772  plyreres  15788  dvply1  15789  dvply2g  15790  efper  15831  sinperlem  15832  abssinper  15870  cxpexprp  15920  logcxp  15922  rpcxpcl  15928  rpcxproot  15939  rprelogbmulexp  15981  lgsval2lem  16043  lgssq2  16074  lgsprme0  16075  ausgrusgrben  16323  wlkepvtx  16530  bj-inex  16847  peano5set  16880  findset  16885  bj-findis  16919  nninfsellemsuc  16960  nninfself  16961  cvgcmp2nlemabs  16986  iooref1o  16988  trilpolemeq1  16994  nconstwlpolemgt0  17019