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  940  3adantr1  1159  3adantr2  1160  3adantr3  1161  syl3anr1  1302  syl3anr3  1304  dfbi3dc  1417  xordidc  1419  elabgt  2921  sbciegft  3036  csbtt  3113  csbnestgf  3154  copsex2t  4307  pofun  4377  onsucmin  4573  onsucelsucr  4574  onsucsssucr  4575  ordsucunielexmid  4597  ordsuc  4629  nlimsucg  4632  elnn  4672  xpsspw  4805  elxp4  5189  elxp5  5190  funimass2  5371  imain  5375  funimaexg  5377  f1ff1  5511  dff1o2  5549  resdif  5566  funbrfv  5640  fvelimab  5658  eqfnfv2  5701  fvimacnvi  5717  ffvresb  5766  fnressn  5793  fmptapd  5798  fnex  5829  rexima  5846  ralima  5847  f1elima  5865  fnotovb  6011  mpoeq12  6028  fovcdm  6112  fnovrn  6117  ofrfval  6190  ofvalg  6191  cofunexg  6217  cofunex2g  6218  mpoexxg  6319  mpoexg  6320  f1o2ndf1  6337  spc2ed  6342  smodm2  6404  tfrlem9  6428  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  tfri3  6476  rdgtfr  6483  rdgruledefgg  6484  oav2  6572  oasuc  6573  omv2  6574  onasuc  6575  omsuc  6581  onmsuc  6582  nnaass  6594  nndi  6595  nndir  6599  nnaword  6620  ecelqsg  6698  iinerm  6717  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  fvdiagfn  6803  ixpssmap2g  6837  domentr  6906  xpdom1g  6953  fopwdom  6958  ssenen  6973  phplem3  6976  phplem4  6977  php5dom  6985  ssfilem  6998  diffitest  7010  ctssdccl  7239  pm54.43  7324  pw1if  7371  addclpi  7475  addasspig  7478  mulasspig  7480  distrpig  7481  mulcanpig  7483  nnppipi  7491  enqdc1  7510  addassnqg  7530  ltbtwnnqq  7563  prarloclemarch  7566  prarloclemarch2  7567  enq0sym  7580  enq0ref  7581  addclnq0  7599  nqpnq0nq  7601  nnanq0  7606  distrnq0  7607  addassnq0lemcl  7609  addassnq0  7610  distnq0r  7611  prarloclemlt  7641  genpassl  7672  genpassu  7673  genpassg  7674  nqpru  7700  addcomprg  7726  mulcomprg  7728  distrlem1prl  7730  distrlem1pru  7731  1idprl  7738  1idpru  7739  recexprlemdisj  7778  recexprlem1ssl  7781  peano2nnnn  8001  ax1rid  8025  axcaucvglemcl  8043  le2tri3i  8216  add4  8268  cnegexlem1  8282  cnegexlem3  8284  cnegex  8285  subadd  8310  addsub  8318  addsubeq4  8322  negdi  8364  renegcl  8368  resubcl  8371  subdi  8492  mulneg2  8503  mul2neg  8505  submul2  8506  ltnegcon2  8572  lenegcon2  8575  lesub0  8587  cru  8710  recextlem1  8759  recexap  8761  div12ap  8802  divnegap  8814  letrp1  8956  dfinfre  9064  peano2nn  9083  nndivre  9107  nnsub  9110  nndivtr  9113  arch  9327  bndndx  9329  nn0addge1  9376  nn0addge2  9377  zaddcl  9447  zsubcl  9448  zltnle  9453  zrevaddcl  9458  nzadd  9460  zleltp1  9463  zltlem1  9465  zdiv  9496  peano2uz2  9515  uzind  9519  eluzp1l  9708  ublbneg  9769  qaddcl  9791  qsubcl  9794  qreccl  9798  qdivcl  9799  qrevaddcl  9800  irradd  9802  irrmul  9803  rerpdivcl  9841  nn0ledivnn  9924  xrre  9977  rexsub  10010  xaddass  10026  xnpcan  10029  xsubge0  10038  xposdif  10039  elioc2  10093  icoshft  10147  iccdil  10155  fzss2  10221  fzsuc2  10236  fzrev2  10242  elfzm11  10248  elfzp1b  10254  fzrevral  10262  fzshftral  10265  fzof  10301  fzoval  10305  fzon  10324  elfzoextl  10357  fzosubel  10360  zpnn0elfzo  10373  elfzom1b  10395  qltnle  10423  flqlt  10463  flqbi  10470  flqaddz  10477  fzofig  10614  seq3feq2  10658  ser3le  10719  expp1  10728  expm1t  10749  expeq0  10752  binom2sub  10835  bernneq  10842  expnlbnd  10846  zzlesq  10890  faccl  10917  facdiv  10920  bcpasc  10948  bccl  10949  ffz0hash  11015  fnfzo0hash  11017  wrdlen1  11068  wrdred1  11073  ccatval21sw  11099  wrdl1exs1  11121  ccatws1cl  11124  ccatws1leng  11126  pfxmpt  11171  pfxfv  11175  pfxfvlsw  11186  ccatpfx  11192  pfx1  11194  swrdccatin1  11216  swrdccat  11226  pfxccatpfx1  11227  2shfti  11257  crim  11284  mulreap  11290  resub  11296  imsub  11304  ipcnval  11312  cjsub  11318  resqrexlemfp1  11435  resqrexlemgt0  11446  sqabsadd  11481  sqabssub  11482  abs2dif2  11533  cau3lem  11540  icodiamlt  11606  xrmaxaddlem  11686  clim  11707  clim2  11709  clim2c  11710  clim0c  11712  2clim  11727  climabs0  11733  climcn1  11734  climcn2  11735  climsqz  11761  climsqz2  11762  climub  11770  climserle  11771  fsum3cvg  11804  fisumss  11818  fsum3ser  11823  sumsplitdc  11858  fsump1i  11859  fsumlessfi  11886  telfsumo  11892  fsumparts  11896  iserabs  11901  binomlem  11909  isumsplit  11917  isum1p  11918  isumlessdc  11922  mertenslem2  11962  mertensabs  11963  prodfap0  11971  prodfrecap  11972  prodfdivap  11973  fproddccvg  11998  prodmodclem2  12003  fprodssdc  12016  fprodabs  12042  fprodeq0  12043  fprodeq0g  12064  ege2le3  12097  efsub  12107  efexp  12108  efsep  12117  sinsub  12166  cossub  12167  demoivre  12199  eirraplem  12203  moddvds  12225  0dvds  12237  iddvdsexp  12241  dvdssub  12264  dvdsle  12270  dvdsleabs  12271  dvdseq  12274  dvdsflip  12277  mulsucdiv2z  12311  divalgb  12351  divalg2  12352  ndvdsadd  12357  bitsp1  12377  gcdneg  12418  gcdabs2  12426  modgcd  12427  bezoutlemsup  12445  gcdmultiplez  12457  gcdeq  12459  dvdssq  12467  lcmcllem  12504  lcmneg  12511  lcmdvds  12516  qredeu  12534  cncongrcoprm  12543  isprm3  12555  prmrp  12582  divnumden  12633  phiprmpw  12659  crth  12661  hashgcdlem  12675  hashgcdeq  12677  modprminv  12687  modprminveq  12688  modprmn0modprm0  12694  coprimeprodsq2  12696  pcpre1  12730  pccl  12737  pcmul  12739  pcdiv  12740  pcqcl  12744  pcexp  12747  pcdvds  12753  pcndvds  12755  pcndvds2  12757  pcelnn  12759  pcgcd1  12766  pc2dvds  12768  pc11  12769  gzsubcl  12818  4sqlem3  12828  setsresg  12985  pwssnf1o  13245  xpsfeq  13292  submcl  13426  grpinvnzcl  13519  mulgnnass  13608  nmzsubg  13661  nmznsg  13664  resghm2b  13713  ghmnsgpreima  13720  gsumfzsnfd  13796  iscrng2  13892  subrngpropd  14093  issubrg3  14124  subrgpropd  14130  islmodd  14170  lss1d  14260  lspsncl  14269  lspsnid  14284  df2idl2  14386  2idlcpbl  14401  qusrhm  14405  gsumfzfsumlemm  14464  iunopn  14589  unopn  14592  eltg  14639  eltg2  14640  tgcl  14651  tgiun  14660  tgidm  14661  isopn3i  14722  isneip  14733  neipsm  14741  restbasg  14755  restopn2  14770  lmbrf  14802  cnclima  14810  lmss  14833  txbasval  14854  txlm  14866  psmetxrge0  14919  blininf  15011  blssps  15014  blss  15015  elmopn2  15036  bdmet  15089  metrest  15093  bl2ioo  15137  dvcjbr  15295  plyaddlem1  15334  plymullem1  15335  plyreres  15351  dvply1  15352  dvply2g  15353  efper  15394  sinperlem  15395  abssinper  15433  cxpexprp  15482  logcxp  15484  rpcxpcl  15490  rpcxproot  15501  rprelogbmulexp  15543  lgsval2lem  15602  lgssq2  15633  lgsprme0  15634  bj-inex  16042  peano5set  16075  findset  16080  bj-findis  16114  nninfsellemsuc  16151  nninfself  16152  cvgcmp2nlemabs  16173  iooref1o  16175  trilpolemeq1  16181  nconstwlpolemgt0  16205