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  2901  sbciegft  3016  csbtt  3092  csbnestgf  3133  copsex2t  4274  pofun  4343  onsucmin  4539  onsucelsucr  4540  onsucsssucr  4541  ordsucunielexmid  4563  ordsuc  4595  nlimsucg  4598  elnn  4638  xpsspw  4771  elxp4  5153  elxp5  5154  funimass2  5332  imain  5336  funimaexg  5338  f1ff1  5467  dff1o2  5505  resdif  5522  funbrfv  5595  fvelimab  5613  eqfnfv2  5656  fvimacnvi  5672  ffvresb  5721  fnressn  5744  fmptapd  5749  fnex  5780  rexima  5797  ralima  5798  f1elima  5816  fnotovb  5961  mpoeq12  5978  fovcdm  6061  fnovrn  6066  ofrfval  6139  ofvalg  6140  cofunexg  6161  cofunex2g  6162  mpoexxg  6263  mpoexg  6264  f1o2ndf1  6281  spc2ed  6286  smodm2  6348  tfrlem9  6372  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  tfri3  6420  rdgtfr  6427  rdgruledefgg  6428  oav2  6516  oasuc  6517  omv2  6518  onasuc  6519  omsuc  6525  onmsuc  6526  nnaass  6538  nndi  6539  nndir  6543  nnaword  6564  ecelqsg  6642  iinerm  6661  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  fvdiagfn  6747  ixpssmap2g  6781  domentr  6845  xpdom1g  6887  fopwdom  6892  ssenen  6907  phplem3  6910  phplem4  6911  php5dom  6919  ssfilem  6931  diffitest  6943  ctssdccl  7170  pm54.43  7250  addclpi  7387  addasspig  7390  mulasspig  7392  distrpig  7393  mulcanpig  7395  nnppipi  7403  enqdc1  7422  addassnqg  7442  ltbtwnnqq  7475  prarloclemarch  7478  prarloclemarch2  7479  enq0sym  7492  enq0ref  7493  addclnq0  7511  nqpnq0nq  7513  nnanq0  7518  distrnq0  7519  addassnq0lemcl  7521  addassnq0  7522  distnq0r  7523  prarloclemlt  7553  genpassl  7584  genpassu  7585  genpassg  7586  nqpru  7612  addcomprg  7638  mulcomprg  7640  distrlem1prl  7642  distrlem1pru  7643  1idprl  7650  1idpru  7651  recexprlemdisj  7690  recexprlem1ssl  7693  peano2nnnn  7913  ax1rid  7937  axcaucvglemcl  7955  le2tri3i  8128  add4  8180  cnegexlem1  8194  cnegexlem3  8196  cnegex  8197  subadd  8222  addsub  8230  addsubeq4  8234  negdi  8276  renegcl  8280  resubcl  8283  subdi  8404  mulneg2  8415  mul2neg  8417  submul2  8418  ltnegcon2  8483  lenegcon2  8486  lesub0  8498  cru  8621  recextlem1  8670  recexap  8672  div12ap  8713  divnegap  8725  letrp1  8867  dfinfre  8975  peano2nn  8994  nndivre  9018  nnsub  9021  nndivtr  9024  arch  9237  bndndx  9239  nn0addge1  9286  nn0addge2  9287  zaddcl  9357  zsubcl  9358  zltnle  9363  zrevaddcl  9367  nzadd  9369  zleltp1  9372  zltlem1  9374  zdiv  9405  peano2uz2  9424  uzind  9428  eluzp1l  9617  ublbneg  9678  qaddcl  9700  qsubcl  9703  qreccl  9707  qdivcl  9708  qrevaddcl  9709  irradd  9711  irrmul  9712  rerpdivcl  9750  nn0ledivnn  9833  xrre  9886  rexsub  9919  xaddass  9935  xnpcan  9938  xsubge0  9947  xposdif  9948  elioc2  10002  icoshft  10056  iccdil  10064  fzss2  10130  fzsuc2  10145  fzrev2  10151  elfzm11  10157  elfzp1b  10163  fzrevral  10171  fzshftral  10174  fzof  10210  fzoval  10214  fzon  10233  fzosubel  10261  zpnn0elfzo  10274  elfzom1b  10296  qltnle  10313  flqlt  10352  flqbi  10359  flqaddz  10366  fzofig  10503  seq3feq2  10547  ser3le  10608  expp1  10617  expm1t  10638  expeq0  10641  binom2sub  10724  bernneq  10731  expnlbnd  10735  zzlesq  10779  faccl  10806  facdiv  10809  bcpasc  10837  bccl  10838  ffz0hash  10904  fnfzo0hash  10906  wrdlen1  10951  wrdred1  10956  2shfti  10975  crim  11002  mulreap  11008  resub  11014  imsub  11022  ipcnval  11030  cjsub  11036  resqrexlemfp1  11153  resqrexlemgt0  11164  sqabsadd  11199  sqabssub  11200  abs2dif2  11251  cau3lem  11258  icodiamlt  11324  xrmaxaddlem  11403  clim  11424  clim2  11426  clim2c  11427  clim0c  11429  2clim  11444  climabs0  11450  climcn1  11451  climcn2  11452  climsqz  11478  climsqz2  11479  climub  11487  climserle  11488  fsum3cvg  11521  fisumss  11535  fsum3ser  11540  sumsplitdc  11575  fsump1i  11576  fsumlessfi  11603  telfsumo  11609  fsumparts  11613  iserabs  11618  binomlem  11626  isumsplit  11634  isum1p  11635  isumlessdc  11639  mertenslem2  11679  mertensabs  11680  prodfap0  11688  prodfrecap  11689  prodfdivap  11690  fproddccvg  11715  prodmodclem2  11720  fprodssdc  11733  fprodabs  11759  fprodeq0  11760  fprodeq0g  11781  ege2le3  11814  efsub  11824  efexp  11825  efsep  11834  sinsub  11883  cossub  11884  demoivre  11916  eirraplem  11920  moddvds  11942  0dvds  11954  iddvdsexp  11958  dvdssub  11981  dvdsle  11986  dvdsleabs  11987  dvdseq  11990  dvdsflip  11993  mulsucdiv2z  12026  divalgb  12066  divalg2  12067  ndvdsadd  12072  gcdneg  12119  gcdabs2  12127  modgcd  12128  bezoutlemsup  12146  gcdmultiplez  12158  gcdeq  12160  dvdssq  12168  lcmcllem  12205  lcmneg  12212  lcmdvds  12217  qredeu  12235  cncongrcoprm  12244  isprm3  12256  prmrp  12283  divnumden  12334  phiprmpw  12360  crth  12362  hashgcdlem  12376  hashgcdeq  12377  modprminv  12387  modprminveq  12388  modprmn0modprm0  12394  coprimeprodsq2  12396  pcpre1  12430  pccl  12437  pcmul  12439  pcdiv  12440  pcqcl  12444  pcexp  12447  pcdvds  12453  pcndvds  12455  pcndvds2  12457  pcelnn  12459  pcgcd1  12466  pc2dvds  12468  pc11  12469  gzsubcl  12518  4sqlem3  12528  setsresg  12656  xpsfeq  12928  submcl  13051  grpinvnzcl  13144  mulgnnass  13227  nmzsubg  13280  nmznsg  13283  resghm2b  13332  ghmnsgpreima  13339  gsumfzsnfd  13415  iscrng2  13511  subrngpropd  13712  issubrg3  13743  subrgpropd  13749  islmodd  13789  lss1d  13879  lspsncl  13888  lspsnid  13903  df2idl2  14005  2idlcpbl  14020  qusrhm  14024  gsumfzfsumlemm  14075  iunopn  14170  unopn  14173  eltg  14220  eltg2  14221  tgcl  14232  tgiun  14241  tgidm  14242  isopn3i  14303  isneip  14314  neipsm  14322  restbasg  14336  restopn2  14351  lmbrf  14383  cnclima  14391  lmss  14414  txbasval  14435  txlm  14447  psmetxrge0  14500  blininf  14592  blssps  14595  blss  14596  elmopn2  14617  bdmet  14670  metrest  14674  bl2ioo  14710  dvcjbr  14857  plyaddlem1  14893  plymullem1  14894  efper  14942  sinperlem  14943  abssinper  14981  cxpexprp  15030  logcxp  15032  rpcxpcl  15038  rpcxproot  15048  rprelogbmulexp  15088  lgsval2lem  15126  lgssq2  15157  lgsprme0  15158  bj-inex  15399  peano5set  15432  findset  15437  bj-findis  15471  nninfsellemsuc  15502  nninfself  15503  cvgcmp2nlemabs  15522  iooref1o  15524  trilpolemeq1  15530  nconstwlpolemgt0  15554