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  2945  sbciegft  3060  csbtt  3137  csbnestgf  3178  copsex2t  4335  pofun  4407  onsucmin  4603  onsucelsucr  4604  onsucsssucr  4605  ordsucunielexmid  4627  ordsuc  4659  nlimsucg  4662  elnn  4702  xpsspw  4836  elxp4  5222  elxp5  5223  funimass2  5405  imain  5409  funimaexg  5411  f1ff1  5547  dff1o2  5585  resdif  5602  funbrfv  5678  fnbrfvb2  5684  fvelimab  5698  eqfnfv2  5741  fvimacnvi  5757  ffvresb  5806  fnressn  5835  fmptapd  5840  fnex  5871  rexima  5890  ralima  5891  f1elima  5909  fnotovb  6059  mpoeq12  6076  fovcdm  6160  fnovrn  6165  ofrfval  6239  ofvalg  6240  cofunexg  6266  cofunex2g  6267  mpoexxg  6370  mpoexg  6371  f1o2ndf1  6388  spc2ed  6393  smodm2  6456  tfrlem9  6480  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  tfri3  6528  rdgtfr  6535  rdgruledefgg  6536  oav2  6626  oasuc  6627  omv2  6628  onasuc  6629  omsuc  6635  onmsuc  6636  nnaass  6648  nndi  6649  nndir  6653  nnaword  6674  ecelqsg  6752  iinerm  6771  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  fvdiagfn  6857  ixpssmap2g  6891  domentr  6960  xpdom1g  7012  fopwdom  7017  ssenen  7032  phplem3  7035  phplem4  7036  php5dom  7044  ssfilem  7057  diffitest  7069  ctssdccl  7301  pm54.43  7386  pw1if  7433  addclpi  7537  addasspig  7540  mulasspig  7542  distrpig  7543  mulcanpig  7545  nnppipi  7553  enqdc1  7572  addassnqg  7592  ltbtwnnqq  7625  prarloclemarch  7628  prarloclemarch2  7629  enq0sym  7642  enq0ref  7643  addclnq0  7661  nqpnq0nq  7663  nnanq0  7668  distrnq0  7669  addassnq0lemcl  7671  addassnq0  7672  distnq0r  7673  prarloclemlt  7703  genpassl  7734  genpassu  7735  genpassg  7736  nqpru  7762  addcomprg  7788  mulcomprg  7790  distrlem1prl  7792  distrlem1pru  7793  1idprl  7800  1idpru  7801  recexprlemdisj  7840  recexprlem1ssl  7843  peano2nnnn  8063  ax1rid  8087  axcaucvglemcl  8105  le2tri3i  8278  add4  8330  cnegexlem1  8344  cnegexlem3  8346  cnegex  8347  subadd  8372  addsub  8380  addsubeq4  8384  negdi  8426  renegcl  8430  resubcl  8433  subdi  8554  mulneg2  8565  mul2neg  8567  submul2  8568  ltnegcon2  8634  lenegcon2  8637  lesub0  8649  cru  8772  recextlem1  8821  recexap  8823  div12ap  8864  divnegap  8876  letrp1  9018  dfinfre  9126  peano2nn  9145  nndivre  9169  nnsub  9172  nndivtr  9175  arch  9389  bndndx  9391  nn0addge1  9438  nn0addge2  9439  zaddcl  9509  zsubcl  9510  zltnle  9515  zrevaddcl  9520  nzadd  9522  zleltp1  9525  zltlem1  9527  zdiv  9558  peano2uz2  9577  uzind  9581  eluzp1l  9771  ublbneg  9837  qaddcl  9859  qsubcl  9862  qreccl  9866  qdivcl  9867  qrevaddcl  9868  irradd  9870  irrmul  9871  rerpdivcl  9909  nn0ledivnn  9992  xrre  10045  rexsub  10078  xaddass  10094  xnpcan  10097  xsubge0  10106  xposdif  10107  elioc2  10161  icoshft  10215  iccdil  10223  fzss2  10289  fzsuc2  10304  fzrev2  10310  elfzm11  10316  elfzp1b  10322  fzrevral  10330  fzshftral  10333  fzof  10369  fzoval  10373  fzon  10392  elfzoextl  10426  fzosubel  10429  zpnn0elfzo  10442  elfzom1b  10464  qltnle  10493  flqlt  10533  flqbi  10540  flqaddz  10547  fzofig  10684  seq3feq2  10728  ser3le  10789  expp1  10798  expm1t  10819  expeq0  10822  binom2sub  10905  bernneq  10912  expnlbnd  10916  zzlesq  10960  faccl  10987  facdiv  10990  bcpasc  11018  bccl  11019  ffz0hash  11087  fnfzo0hash  11089  wrdlen1  11141  wrdred1  11146  ccatval21sw  11172  wrdl1exs1  11196  ccatws1cl  11199  ccatws1leng  11201  pfxmpt  11251  pfxfv  11255  pfxfvlsw  11266  ccatpfx  11272  pfx1  11274  swrdccatin1  11296  swrdccat  11306  pfxccatpfx1  11307  2shfti  11382  crim  11409  mulreap  11415  resub  11421  imsub  11429  ipcnval  11437  cjsub  11443  resqrexlemfp1  11560  resqrexlemgt0  11571  sqabsadd  11606  sqabssub  11607  abs2dif2  11658  cau3lem  11665  icodiamlt  11731  xrmaxaddlem  11811  clim  11832  clim2  11834  clim2c  11835  clim0c  11837  2clim  11852  climabs0  11858  climcn1  11859  climcn2  11860  climsqz  11886  climsqz2  11887  climub  11895  climserle  11896  fsum3cvg  11929  fisumss  11943  fsum3ser  11948  sumsplitdc  11983  fsump1i  11984  fsumlessfi  12011  telfsumo  12017  fsumparts  12021  iserabs  12026  binomlem  12034  isumsplit  12042  isum1p  12043  isumlessdc  12047  mertenslem2  12087  mertensabs  12088  prodfap0  12096  prodfrecap  12097  prodfdivap  12098  fproddccvg  12123  prodmodclem2  12128  fprodssdc  12141  fprodabs  12167  fprodeq0  12168  fprodeq0g  12189  ege2le3  12222  efsub  12232  efexp  12233  efsep  12242  sinsub  12291  cossub  12292  demoivre  12324  eirraplem  12328  moddvds  12350  0dvds  12362  iddvdsexp  12366  dvdssub  12389  dvdsle  12395  dvdsleabs  12396  dvdseq  12399  dvdsflip  12402  mulsucdiv2z  12436  divalgb  12476  divalg2  12477  ndvdsadd  12482  bitsp1  12502  gcdneg  12543  gcdabs2  12551  modgcd  12552  bezoutlemsup  12570  gcdmultiplez  12582  gcdeq  12584  dvdssq  12592  lcmcllem  12629  lcmneg  12636  lcmdvds  12641  qredeu  12659  cncongrcoprm  12668  isprm3  12680  prmrp  12707  divnumden  12758  phiprmpw  12784  crth  12786  hashgcdlem  12800  hashgcdeq  12802  modprminv  12812  modprminveq  12813  modprmn0modprm0  12819  coprimeprodsq2  12821  pcpre1  12855  pccl  12862  pcmul  12864  pcdiv  12865  pcqcl  12869  pcexp  12872  pcdvds  12878  pcndvds  12880  pcndvds2  12882  pcelnn  12884  pcgcd1  12891  pc2dvds  12893  pc11  12894  gzsubcl  12943  4sqlem3  12953  setsresg  13110  pwssnf1o  13371  xpsfeq  13418  submcl  13552  grpinvnzcl  13645  mulgnnass  13734  nmzsubg  13787  nmznsg  13790  resghm2b  13839  ghmnsgpreima  13846  gsumfzsnfd  13922  iscrng2  14018  subrngpropd  14220  issubrg3  14251  subrgpropd  14257  islmodd  14297  lss1d  14387  lspsncl  14396  lspsnid  14411  df2idl2  14513  2idlcpbl  14528  qusrhm  14532  gsumfzfsumlemm  14591  iunopn  14716  unopn  14719  eltg  14766  eltg2  14767  tgcl  14778  tgiun  14787  tgidm  14788  isopn3i  14849  isneip  14860  neipsm  14868  restbasg  14882  restopn2  14897  lmbrf  14929  cnclima  14937  lmss  14960  txbasval  14981  txlm  14993  psmetxrge0  15046  blininf  15138  blssps  15141  blss  15142  elmopn2  15163  bdmet  15216  metrest  15220  bl2ioo  15264  dvcjbr  15422  plyaddlem1  15461  plymullem1  15462  plyreres  15478  dvply1  15479  dvply2g  15480  efper  15521  sinperlem  15522  abssinper  15560  cxpexprp  15609  logcxp  15611  rpcxpcl  15617  rpcxproot  15628  rprelogbmulexp  15670  lgsval2lem  15729  lgssq2  15760  lgsprme0  15761  ausgrusgrben  16007  bj-inex  16438  peano5set  16471  findset  16476  bj-findis  16510  nninfsellemsuc  16550  nninfself  16551  cvgcmp2nlemabs  16572  iooref1o  16574  trilpolemeq1  16580  nconstwlpolemgt0  16604