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  4331  pofun  4403  onsucmin  4599  onsucelsucr  4600  onsucsssucr  4601  ordsucunielexmid  4623  ordsuc  4655  nlimsucg  4658  elnn  4698  xpsspw  4831  elxp4  5216  elxp5  5217  funimass2  5399  imain  5403  funimaexg  5405  f1ff1  5541  dff1o2  5579  resdif  5596  funbrfv  5672  fnbrfvb2  5678  fvelimab  5692  eqfnfv2  5735  fvimacnvi  5751  ffvresb  5800  fnressn  5829  fmptapd  5834  fnex  5865  rexima  5884  ralima  5885  f1elima  5903  fnotovb  6053  mpoeq12  6070  fovcdm  6154  fnovrn  6159  ofrfval  6233  ofvalg  6234  cofunexg  6260  cofunex2g  6261  mpoexxg  6362  mpoexg  6363  f1o2ndf1  6380  spc2ed  6385  smodm2  6447  tfrlem9  6471  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  tfri3  6519  rdgtfr  6526  rdgruledefgg  6527  oav2  6617  oasuc  6618  omv2  6619  onasuc  6620  omsuc  6626  onmsuc  6627  nnaass  6639  nndi  6640  nndir  6644  nnaword  6665  ecelqsg  6743  iinerm  6762  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  fvdiagfn  6848  ixpssmap2g  6882  domentr  6951  xpdom1g  7000  fopwdom  7005  ssenen  7020  phplem3  7023  phplem4  7024  php5dom  7032  ssfilem  7045  diffitest  7057  ctssdccl  7289  pm54.43  7374  pw1if  7421  addclpi  7525  addasspig  7528  mulasspig  7530  distrpig  7531  mulcanpig  7533  nnppipi  7541  enqdc1  7560  addassnqg  7580  ltbtwnnqq  7613  prarloclemarch  7616  prarloclemarch2  7617  enq0sym  7630  enq0ref  7631  addclnq0  7649  nqpnq0nq  7651  nnanq0  7656  distrnq0  7657  addassnq0lemcl  7659  addassnq0  7660  distnq0r  7661  prarloclemlt  7691  genpassl  7722  genpassu  7723  genpassg  7724  nqpru  7750  addcomprg  7776  mulcomprg  7778  distrlem1prl  7780  distrlem1pru  7781  1idprl  7788  1idpru  7789  recexprlemdisj  7828  recexprlem1ssl  7831  peano2nnnn  8051  ax1rid  8075  axcaucvglemcl  8093  le2tri3i  8266  add4  8318  cnegexlem1  8332  cnegexlem3  8334  cnegex  8335  subadd  8360  addsub  8368  addsubeq4  8372  negdi  8414  renegcl  8418  resubcl  8421  subdi  8542  mulneg2  8553  mul2neg  8555  submul2  8556  ltnegcon2  8622  lenegcon2  8625  lesub0  8637  cru  8760  recextlem1  8809  recexap  8811  div12ap  8852  divnegap  8864  letrp1  9006  dfinfre  9114  peano2nn  9133  nndivre  9157  nnsub  9160  nndivtr  9163  arch  9377  bndndx  9379  nn0addge1  9426  nn0addge2  9427  zaddcl  9497  zsubcl  9498  zltnle  9503  zrevaddcl  9508  nzadd  9510  zleltp1  9513  zltlem1  9515  zdiv  9546  peano2uz2  9565  uzind  9569  eluzp1l  9759  ublbneg  9820  qaddcl  9842  qsubcl  9845  qreccl  9849  qdivcl  9850  qrevaddcl  9851  irradd  9853  irrmul  9854  rerpdivcl  9892  nn0ledivnn  9975  xrre  10028  rexsub  10061  xaddass  10077  xnpcan  10080  xsubge0  10089  xposdif  10090  elioc2  10144  icoshft  10198  iccdil  10206  fzss2  10272  fzsuc2  10287  fzrev2  10293  elfzm11  10299  elfzp1b  10305  fzrevral  10313  fzshftral  10316  fzof  10352  fzoval  10356  fzon  10375  elfzoextl  10409  fzosubel  10412  zpnn0elfzo  10425  elfzom1b  10447  qltnle  10475  flqlt  10515  flqbi  10522  flqaddz  10529  fzofig  10666  seq3feq2  10710  ser3le  10771  expp1  10780  expm1t  10801  expeq0  10804  binom2sub  10887  bernneq  10894  expnlbnd  10898  zzlesq  10942  faccl  10969  facdiv  10972  bcpasc  11000  bccl  11001  ffz0hash  11068  fnfzo0hash  11070  wrdlen1  11122  wrdred1  11127  ccatval21sw  11153  wrdl1exs1  11177  ccatws1cl  11180  ccatws1leng  11182  pfxmpt  11227  pfxfv  11231  pfxfvlsw  11242  ccatpfx  11248  pfx1  11250  swrdccatin1  11272  swrdccat  11282  pfxccatpfx1  11283  2shfti  11357  crim  11384  mulreap  11390  resub  11396  imsub  11404  ipcnval  11412  cjsub  11418  resqrexlemfp1  11535  resqrexlemgt0  11546  sqabsadd  11581  sqabssub  11582  abs2dif2  11633  cau3lem  11640  icodiamlt  11706  xrmaxaddlem  11786  clim  11807  clim2  11809  clim2c  11810  clim0c  11812  2clim  11827  climabs0  11833  climcn1  11834  climcn2  11835  climsqz  11861  climsqz2  11862  climub  11870  climserle  11871  fsum3cvg  11904  fisumss  11918  fsum3ser  11923  sumsplitdc  11958  fsump1i  11959  fsumlessfi  11986  telfsumo  11992  fsumparts  11996  iserabs  12001  binomlem  12009  isumsplit  12017  isum1p  12018  isumlessdc  12022  mertenslem2  12062  mertensabs  12063  prodfap0  12071  prodfrecap  12072  prodfdivap  12073  fproddccvg  12098  prodmodclem2  12103  fprodssdc  12116  fprodabs  12142  fprodeq0  12143  fprodeq0g  12164  ege2le3  12197  efsub  12207  efexp  12208  efsep  12217  sinsub  12266  cossub  12267  demoivre  12299  eirraplem  12303  moddvds  12325  0dvds  12337  iddvdsexp  12341  dvdssub  12364  dvdsle  12370  dvdsleabs  12371  dvdseq  12374  dvdsflip  12377  mulsucdiv2z  12411  divalgb  12451  divalg2  12452  ndvdsadd  12457  bitsp1  12477  gcdneg  12518  gcdabs2  12526  modgcd  12527  bezoutlemsup  12545  gcdmultiplez  12557  gcdeq  12559  dvdssq  12567  lcmcllem  12604  lcmneg  12611  lcmdvds  12616  qredeu  12634  cncongrcoprm  12643  isprm3  12655  prmrp  12682  divnumden  12733  phiprmpw  12759  crth  12761  hashgcdlem  12775  hashgcdeq  12777  modprminv  12787  modprminveq  12788  modprmn0modprm0  12794  coprimeprodsq2  12796  pcpre1  12830  pccl  12837  pcmul  12839  pcdiv  12840  pcqcl  12844  pcexp  12847  pcdvds  12853  pcndvds  12855  pcndvds2  12857  pcelnn  12859  pcgcd1  12866  pc2dvds  12868  pc11  12869  gzsubcl  12918  4sqlem3  12928  setsresg  13085  pwssnf1o  13346  xpsfeq  13393  submcl  13527  grpinvnzcl  13620  mulgnnass  13709  nmzsubg  13762  nmznsg  13765  resghm2b  13814  ghmnsgpreima  13821  gsumfzsnfd  13897  iscrng2  13993  subrngpropd  14195  issubrg3  14226  subrgpropd  14232  islmodd  14272  lss1d  14362  lspsncl  14371  lspsnid  14386  df2idl2  14488  2idlcpbl  14503  qusrhm  14507  gsumfzfsumlemm  14566  iunopn  14691  unopn  14694  eltg  14741  eltg2  14742  tgcl  14753  tgiun  14762  tgidm  14763  isopn3i  14824  isneip  14835  neipsm  14843  restbasg  14857  restopn2  14872  lmbrf  14904  cnclima  14912  lmss  14935  txbasval  14956  txlm  14968  psmetxrge0  15021  blininf  15113  blssps  15116  blss  15117  elmopn2  15138  bdmet  15191  metrest  15195  bl2ioo  15239  dvcjbr  15397  plyaddlem1  15436  plymullem1  15437  plyreres  15453  dvply1  15454  dvply2g  15455  efper  15496  sinperlem  15497  abssinper  15535  cxpexprp  15584  logcxp  15586  rpcxpcl  15592  rpcxproot  15603  rprelogbmulexp  15645  lgsval2lem  15704  lgssq2  15735  lgsprme0  15736  ausgrusgrben  15981  bj-inex  16325  peano5set  16358  findset  16363  bj-findis  16397  nninfsellemsuc  16438  nninfself  16439  cvgcmp2nlemabs  16460  iooref1o  16462  trilpolemeq1  16468  nconstwlpolemgt0  16492