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  568  annimdc  945  ifpnst  996  3adantr1  1182  3adantr2  1183  3adantr3  1184  syl3anr1  1325  syl3anr3  1327  dfbi3dc  1441  xordidc  1443  elabgt  2947  sbciegft  3062  csbtt  3139  csbnestgf  3180  copsex2t  4337  pofun  4409  onsucmin  4605  onsucelsucr  4606  onsucsssucr  4607  ordsucunielexmid  4629  ordsuc  4661  nlimsucg  4664  elnn  4704  xpsspw  4838  elxp4  5224  elxp5  5225  funimass2  5408  imain  5412  funimaexg  5414  f1ff1  5550  dff1o2  5588  resdif  5605  funbrfv  5682  fnbrfvb2  5688  fvelimab  5702  eqfnfv2  5745  fvimacnvi  5761  ffvresb  5810  fnressn  5840  fmptapd  5845  fnex  5876  rexima  5895  ralima  5896  f1elima  5914  fnotovb  6064  mpoeq12  6081  fovcdm  6165  fnovrn  6170  ofrfval  6244  ofvalg  6245  cofunexg  6271  cofunex2g  6272  mpoexxg  6375  mpoexg  6376  f1o2ndf1  6393  spc2ed  6398  smodm2  6461  tfrlem9  6485  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  tfri3  6533  rdgtfr  6540  rdgruledefgg  6541  oav2  6631  oasuc  6632  omv2  6633  onasuc  6634  omsuc  6640  onmsuc  6641  nnaass  6653  nndi  6654  nndir  6658  nnaword  6679  ecelqsg  6757  iinerm  6776  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  fvdiagfn  6862  ixpssmap2g  6896  domentr  6965  xpdom1g  7017  fopwdom  7022  ssenen  7037  phplem3  7040  phplem4  7041  php5dom  7049  ssfilem  7062  ssfilemd  7064  diffitest  7076  ctssdccl  7310  pm54.43  7395  pw1if  7443  addclpi  7547  addasspig  7550  mulasspig  7552  distrpig  7553  mulcanpig  7555  nnppipi  7563  enqdc1  7582  addassnqg  7602  ltbtwnnqq  7635  prarloclemarch  7638  prarloclemarch2  7639  enq0sym  7652  enq0ref  7653  addclnq0  7671  nqpnq0nq  7673  nnanq0  7678  distrnq0  7679  addassnq0lemcl  7681  addassnq0  7682  distnq0r  7683  prarloclemlt  7713  genpassl  7744  genpassu  7745  genpassg  7746  nqpru  7772  addcomprg  7798  mulcomprg  7800  distrlem1prl  7802  distrlem1pru  7803  1idprl  7810  1idpru  7811  recexprlemdisj  7850  recexprlem1ssl  7853  peano2nnnn  8073  ax1rid  8097  axcaucvglemcl  8115  le2tri3i  8288  add4  8340  cnegexlem1  8354  cnegexlem3  8356  cnegex  8357  subadd  8382  addsub  8390  addsubeq4  8394  negdi  8436  renegcl  8440  resubcl  8443  subdi  8564  mulneg2  8575  mul2neg  8577  submul2  8578  ltnegcon2  8644  lenegcon2  8647  lesub0  8659  cru  8782  recextlem1  8831  recexap  8833  div12ap  8874  divnegap  8886  letrp1  9028  dfinfre  9136  peano2nn  9155  nndivre  9179  nnsub  9182  nndivtr  9185  arch  9399  bndndx  9401  nn0addge1  9448  nn0addge2  9449  zaddcl  9519  zsubcl  9520  zltnle  9525  zrevaddcl  9530  nzadd  9532  zleltp1  9535  zltlem1  9537  zdiv  9568  peano2uz2  9587  uzind  9591  eluzp1l  9781  ublbneg  9847  qaddcl  9869  qsubcl  9872  qreccl  9876  qdivcl  9877  qrevaddcl  9878  irradd  9880  irrmul  9881  rerpdivcl  9919  nn0ledivnn  10002  xrre  10055  rexsub  10088  xaddass  10104  xnpcan  10107  xsubge0  10116  xposdif  10117  elioc2  10171  icoshft  10225  iccdil  10233  fzss2  10299  fzsuc2  10314  fzrev2  10320  elfzm11  10326  elfzp1b  10332  fzrevral  10340  fzshftral  10343  fzof  10379  fzoval  10383  fzon  10402  elfzoextl  10437  fzosubel  10440  zpnn0elfzo  10453  elfzom1b  10475  qltnle  10504  flqlt  10544  flqbi  10551  flqaddz  10558  fzofig  10695  seq3feq2  10739  ser3le  10800  expp1  10809  expm1t  10830  expeq0  10833  binom2sub  10916  bernneq  10923  expnlbnd  10927  zzlesq  10971  faccl  10998  facdiv  11001  bcpasc  11029  bccl  11030  ffz0hash  11098  fnfzo0hash  11100  wrdlen1  11155  wrdred1  11160  ccatval21sw  11186  wrdl1exs1  11210  ccatws1cl  11213  ccatws1leng  11215  pfxmpt  11265  pfxfv  11269  pfxfvlsw  11280  ccatpfx  11286  pfx1  11288  swrdccatin1  11310  swrdccat  11320  pfxccatpfx1  11321  2shfti  11409  crim  11436  mulreap  11442  resub  11448  imsub  11456  ipcnval  11464  cjsub  11470  resqrexlemfp1  11587  resqrexlemgt0  11598  sqabsadd  11633  sqabssub  11634  abs2dif2  11685  cau3lem  11692  icodiamlt  11758  xrmaxaddlem  11838  clim  11859  clim2  11861  clim2c  11862  clim0c  11864  2clim  11879  climabs0  11885  climcn1  11886  climcn2  11887  climsqz  11913  climsqz2  11914  climub  11922  climserle  11923  fsum3cvg  11957  fisumss  11971  fsum3ser  11976  sumsplitdc  12011  fsump1i  12012  fsumlessfi  12039  telfsumo  12045  fsumparts  12049  iserabs  12054  binomlem  12062  isumsplit  12070  isum1p  12071  isumlessdc  12075  mertenslem2  12115  mertensabs  12116  prodfap0  12124  prodfrecap  12125  prodfdivap  12126  fproddccvg  12151  prodmodclem2  12156  fprodssdc  12169  fprodabs  12195  fprodeq0  12196  fprodeq0g  12217  ege2le3  12250  efsub  12260  efexp  12261  efsep  12270  sinsub  12319  cossub  12320  demoivre  12352  eirraplem  12356  moddvds  12378  0dvds  12390  iddvdsexp  12394  dvdssub  12417  dvdsle  12423  dvdsleabs  12424  dvdseq  12427  dvdsflip  12430  mulsucdiv2z  12464  divalgb  12504  divalg2  12505  ndvdsadd  12510  bitsp1  12530  gcdneg  12571  gcdabs2  12579  modgcd  12580  bezoutlemsup  12598  gcdmultiplez  12610  gcdeq  12612  dvdssq  12620  lcmcllem  12657  lcmneg  12664  lcmdvds  12669  qredeu  12687  cncongrcoprm  12696  isprm3  12708  prmrp  12735  divnumden  12786  phiprmpw  12812  crth  12814  hashgcdlem  12828  hashgcdeq  12830  modprminv  12840  modprminveq  12841  modprmn0modprm0  12847  coprimeprodsq2  12849  pcpre1  12883  pccl  12890  pcmul  12892  pcdiv  12893  pcqcl  12897  pcexp  12900  pcdvds  12906  pcndvds  12908  pcndvds2  12910  pcelnn  12912  pcgcd1  12919  pc2dvds  12921  pc11  12922  gzsubcl  12971  4sqlem3  12981  setsresg  13138  pwssnf1o  13399  xpsfeq  13446  submcl  13580  grpinvnzcl  13673  mulgnnass  13762  nmzsubg  13815  nmznsg  13818  resghm2b  13867  ghmnsgpreima  13874  gsumfzsnfd  13950  iscrng2  14047  subrngpropd  14249  issubrg3  14280  subrgpropd  14286  islmodd  14326  lss1d  14416  lspsncl  14425  lspsnid  14440  df2idl2  14542  2idlcpbl  14557  qusrhm  14561  gsumfzfsumlemm  14620  iunopn  14745  unopn  14748  eltg  14795  eltg2  14796  tgcl  14807  tgiun  14816  tgidm  14817  isopn3i  14878  isneip  14889  neipsm  14897  restbasg  14911  restopn2  14926  lmbrf  14958  cnclima  14966  lmss  14989  txbasval  15010  txlm  15022  psmetxrge0  15075  blininf  15167  blssps  15170  blss  15171  elmopn2  15192  bdmet  15245  metrest  15249  bl2ioo  15293  dvcjbr  15451  plyaddlem1  15490  plymullem1  15491  plyreres  15507  dvply1  15508  dvply2g  15509  efper  15550  sinperlem  15551  abssinper  15589  cxpexprp  15638  logcxp  15640  rpcxpcl  15646  rpcxproot  15657  rprelogbmulexp  15699  lgsval2lem  15758  lgssq2  15789  lgsprme0  15790  ausgrusgrben  16038  wlkepvtx  16245  bj-inex  16553  peano5set  16586  findset  16591  bj-findis  16625  nninfsellemsuc  16665  nninfself  16666  cvgcmp2nlemabs  16687  iooref1o  16689  trilpolemeq1  16695  nconstwlpolemgt0  16720