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  2914  sbciegft  3029  csbtt  3105  csbnestgf  3146  copsex2t  4289  pofun  4359  onsucmin  4555  onsucelsucr  4556  onsucsssucr  4557  ordsucunielexmid  4579  ordsuc  4611  nlimsucg  4614  elnn  4654  xpsspw  4787  elxp4  5170  elxp5  5171  funimass2  5352  imain  5356  funimaexg  5358  f1ff1  5489  dff1o2  5527  resdif  5544  funbrfv  5617  fvelimab  5635  eqfnfv2  5678  fvimacnvi  5694  ffvresb  5743  fnressn  5770  fmptapd  5775  fnex  5806  rexima  5823  ralima  5824  f1elima  5842  fnotovb  5988  mpoeq12  6005  fovcdm  6089  fnovrn  6094  ofrfval  6167  ofvalg  6168  cofunexg  6194  cofunex2g  6195  mpoexxg  6296  mpoexg  6297  f1o2ndf1  6314  spc2ed  6319  smodm2  6381  tfrlem9  6405  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  tfri3  6453  rdgtfr  6460  rdgruledefgg  6461  oav2  6549  oasuc  6550  omv2  6551  onasuc  6552  omsuc  6558  onmsuc  6559  nnaass  6571  nndi  6572  nndir  6576  nnaword  6597  ecelqsg  6675  iinerm  6694  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  fvdiagfn  6780  ixpssmap2g  6814  domentr  6883  xpdom1g  6928  fopwdom  6933  ssenen  6948  phplem3  6951  phplem4  6952  php5dom  6960  ssfilem  6972  diffitest  6984  ctssdccl  7213  pm54.43  7298  addclpi  7440  addasspig  7443  mulasspig  7445  distrpig  7446  mulcanpig  7448  nnppipi  7456  enqdc1  7475  addassnqg  7495  ltbtwnnqq  7528  prarloclemarch  7531  prarloclemarch2  7532  enq0sym  7545  enq0ref  7546  addclnq0  7564  nqpnq0nq  7566  nnanq0  7571  distrnq0  7572  addassnq0lemcl  7574  addassnq0  7575  distnq0r  7576  prarloclemlt  7606  genpassl  7637  genpassu  7638  genpassg  7639  nqpru  7665  addcomprg  7691  mulcomprg  7693  distrlem1prl  7695  distrlem1pru  7696  1idprl  7703  1idpru  7704  recexprlemdisj  7743  recexprlem1ssl  7746  peano2nnnn  7966  ax1rid  7990  axcaucvglemcl  8008  le2tri3i  8181  add4  8233  cnegexlem1  8247  cnegexlem3  8249  cnegex  8250  subadd  8275  addsub  8283  addsubeq4  8287  negdi  8329  renegcl  8333  resubcl  8336  subdi  8457  mulneg2  8468  mul2neg  8470  submul2  8471  ltnegcon2  8537  lenegcon2  8540  lesub0  8552  cru  8675  recextlem1  8724  recexap  8726  div12ap  8767  divnegap  8779  letrp1  8921  dfinfre  9029  peano2nn  9048  nndivre  9072  nnsub  9075  nndivtr  9078  arch  9292  bndndx  9294  nn0addge1  9341  nn0addge2  9342  zaddcl  9412  zsubcl  9413  zltnle  9418  zrevaddcl  9423  nzadd  9425  zleltp1  9428  zltlem1  9430  zdiv  9461  peano2uz2  9480  uzind  9484  eluzp1l  9673  ublbneg  9734  qaddcl  9756  qsubcl  9759  qreccl  9763  qdivcl  9764  qrevaddcl  9765  irradd  9767  irrmul  9768  rerpdivcl  9806  nn0ledivnn  9889  xrre  9942  rexsub  9975  xaddass  9991  xnpcan  9994  xsubge0  10003  xposdif  10004  elioc2  10058  icoshft  10112  iccdil  10120  fzss2  10186  fzsuc2  10201  fzrev2  10207  elfzm11  10213  elfzp1b  10219  fzrevral  10227  fzshftral  10230  fzof  10266  fzoval  10270  fzon  10289  elfzoextl  10320  fzosubel  10323  zpnn0elfzo  10336  elfzom1b  10358  qltnle  10386  flqlt  10426  flqbi  10433  flqaddz  10440  fzofig  10577  seq3feq2  10621  ser3le  10682  expp1  10691  expm1t  10712  expeq0  10715  binom2sub  10798  bernneq  10805  expnlbnd  10809  zzlesq  10853  faccl  10880  facdiv  10883  bcpasc  10911  bccl  10912  ffz0hash  10978  fnfzo0hash  10980  wrdlen1  11031  wrdred1  11036  ccatval21sw  11061  wrdl1exs1  11083  ccatws1cl  11086  ccatws1leng  11088  2shfti  11142  crim  11169  mulreap  11175  resub  11181  imsub  11189  ipcnval  11197  cjsub  11203  resqrexlemfp1  11320  resqrexlemgt0  11331  sqabsadd  11366  sqabssub  11367  abs2dif2  11418  cau3lem  11425  icodiamlt  11491  xrmaxaddlem  11571  clim  11592  clim2  11594  clim2c  11595  clim0c  11597  2clim  11612  climabs0  11618  climcn1  11619  climcn2  11620  climsqz  11646  climsqz2  11647  climub  11655  climserle  11656  fsum3cvg  11689  fisumss  11703  fsum3ser  11708  sumsplitdc  11743  fsump1i  11744  fsumlessfi  11771  telfsumo  11777  fsumparts  11781  iserabs  11786  binomlem  11794  isumsplit  11802  isum1p  11803  isumlessdc  11807  mertenslem2  11847  mertensabs  11848  prodfap0  11856  prodfrecap  11857  prodfdivap  11858  fproddccvg  11883  prodmodclem2  11888  fprodssdc  11901  fprodabs  11927  fprodeq0  11928  fprodeq0g  11949  ege2le3  11982  efsub  11992  efexp  11993  efsep  12002  sinsub  12051  cossub  12052  demoivre  12084  eirraplem  12088  moddvds  12110  0dvds  12122  iddvdsexp  12126  dvdssub  12149  dvdsle  12155  dvdsleabs  12156  dvdseq  12159  dvdsflip  12162  mulsucdiv2z  12196  divalgb  12236  divalg2  12237  ndvdsadd  12242  bitsp1  12262  gcdneg  12303  gcdabs2  12311  modgcd  12312  bezoutlemsup  12330  gcdmultiplez  12342  gcdeq  12344  dvdssq  12352  lcmcllem  12389  lcmneg  12396  lcmdvds  12401  qredeu  12419  cncongrcoprm  12428  isprm3  12440  prmrp  12467  divnumden  12518  phiprmpw  12544  crth  12546  hashgcdlem  12560  hashgcdeq  12562  modprminv  12572  modprminveq  12573  modprmn0modprm0  12579  coprimeprodsq2  12581  pcpre1  12615  pccl  12622  pcmul  12624  pcdiv  12625  pcqcl  12629  pcexp  12632  pcdvds  12638  pcndvds  12640  pcndvds2  12642  pcelnn  12644  pcgcd1  12651  pc2dvds  12653  pc11  12654  gzsubcl  12703  4sqlem3  12713  setsresg  12870  pwssnf1o  13130  xpsfeq  13177  submcl  13311  grpinvnzcl  13404  mulgnnass  13493  nmzsubg  13546  nmznsg  13549  resghm2b  13598  ghmnsgpreima  13605  gsumfzsnfd  13681  iscrng2  13777  subrngpropd  13978  issubrg3  14009  subrgpropd  14015  islmodd  14055  lss1d  14145  lspsncl  14154  lspsnid  14169  df2idl2  14271  2idlcpbl  14286  qusrhm  14290  gsumfzfsumlemm  14349  iunopn  14474  unopn  14477  eltg  14524  eltg2  14525  tgcl  14536  tgiun  14545  tgidm  14546  isopn3i  14607  isneip  14618  neipsm  14626  restbasg  14640  restopn2  14655  lmbrf  14687  cnclima  14695  lmss  14718  txbasval  14739  txlm  14751  psmetxrge0  14804  blininf  14896  blssps  14899  blss  14900  elmopn2  14921  bdmet  14974  metrest  14978  bl2ioo  15022  dvcjbr  15180  plyaddlem1  15219  plymullem1  15220  plyreres  15236  dvply1  15237  dvply2g  15238  efper  15279  sinperlem  15280  abssinper  15318  cxpexprp  15367  logcxp  15369  rpcxpcl  15375  rpcxproot  15386  rprelogbmulexp  15428  lgsval2lem  15487  lgssq2  15518  lgsprme0  15519  bj-inex  15843  peano5set  15876  findset  15881  bj-findis  15915  nninfsellemsuc  15949  nninfself  15950  cvgcmp2nlemabs  15971  iooref1o  15973  trilpolemeq1  15979  nconstwlpolemgt0  16003