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  5839  fmptapd  5844  fnex  5875  rexima  5894  ralima  5895  f1elima  5913  fnotovb  6063  mpoeq12  6080  fovcdm  6164  fnovrn  6169  ofrfval  6243  ofvalg  6244  cofunexg  6270  cofunex2g  6271  mpoexxg  6374  mpoexg  6375  f1o2ndf1  6392  spc2ed  6397  smodm2  6460  tfrlem9  6484  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  tfri3  6532  rdgtfr  6539  rdgruledefgg  6540  oav2  6630  oasuc  6631  omv2  6632  onasuc  6633  omsuc  6639  onmsuc  6640  nnaass  6652  nndi  6653  nndir  6657  nnaword  6678  ecelqsg  6756  iinerm  6775  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  fvdiagfn  6861  ixpssmap2g  6895  domentr  6964  xpdom1g  7016  fopwdom  7021  ssenen  7036  phplem3  7039  phplem4  7040  php5dom  7048  ssfilem  7061  ssfilemd  7063  diffitest  7075  ctssdccl  7309  pm54.43  7394  pw1if  7442  addclpi  7546  addasspig  7549  mulasspig  7551  distrpig  7552  mulcanpig  7554  nnppipi  7562  enqdc1  7581  addassnqg  7601  ltbtwnnqq  7634  prarloclemarch  7637  prarloclemarch2  7638  enq0sym  7651  enq0ref  7652  addclnq0  7670  nqpnq0nq  7672  nnanq0  7677  distrnq0  7678  addassnq0lemcl  7680  addassnq0  7681  distnq0r  7682  prarloclemlt  7712  genpassl  7743  genpassu  7744  genpassg  7745  nqpru  7771  addcomprg  7797  mulcomprg  7799  distrlem1prl  7801  distrlem1pru  7802  1idprl  7809  1idpru  7810  recexprlemdisj  7849  recexprlem1ssl  7852  peano2nnnn  8072  ax1rid  8096  axcaucvglemcl  8114  le2tri3i  8287  add4  8339  cnegexlem1  8353  cnegexlem3  8355  cnegex  8356  subadd  8381  addsub  8389  addsubeq4  8393  negdi  8435  renegcl  8439  resubcl  8442  subdi  8563  mulneg2  8574  mul2neg  8576  submul2  8577  ltnegcon2  8643  lenegcon2  8646  lesub0  8658  cru  8781  recextlem1  8830  recexap  8832  div12ap  8873  divnegap  8885  letrp1  9027  dfinfre  9135  peano2nn  9154  nndivre  9178  nnsub  9181  nndivtr  9184  arch  9398  bndndx  9400  nn0addge1  9447  nn0addge2  9448  zaddcl  9518  zsubcl  9519  zltnle  9524  zrevaddcl  9529  nzadd  9531  zleltp1  9534  zltlem1  9536  zdiv  9567  peano2uz2  9586  uzind  9590  eluzp1l  9780  ublbneg  9846  qaddcl  9868  qsubcl  9871  qreccl  9875  qdivcl  9876  qrevaddcl  9877  irradd  9879  irrmul  9880  rerpdivcl  9918  nn0ledivnn  10001  xrre  10054  rexsub  10087  xaddass  10103  xnpcan  10106  xsubge0  10115  xposdif  10116  elioc2  10170  icoshft  10224  iccdil  10232  fzss2  10298  fzsuc2  10313  fzrev2  10319  elfzm11  10325  elfzp1b  10331  fzrevral  10339  fzshftral  10342  fzof  10378  fzoval  10382  fzon  10401  elfzoextl  10435  fzosubel  10438  zpnn0elfzo  10451  elfzom1b  10473  qltnle  10502  flqlt  10542  flqbi  10549  flqaddz  10556  fzofig  10693  seq3feq2  10737  ser3le  10798  expp1  10807  expm1t  10828  expeq0  10831  binom2sub  10914  bernneq  10921  expnlbnd  10925  zzlesq  10969  faccl  10996  facdiv  10999  bcpasc  11027  bccl  11028  ffz0hash  11096  fnfzo0hash  11098  wrdlen1  11150  wrdred1  11155  ccatval21sw  11181  wrdl1exs1  11205  ccatws1cl  11208  ccatws1leng  11210  pfxmpt  11260  pfxfv  11264  pfxfvlsw  11275  ccatpfx  11281  pfx1  11283  swrdccatin1  11305  swrdccat  11315  pfxccatpfx1  11316  2shfti  11391  crim  11418  mulreap  11424  resub  11430  imsub  11438  ipcnval  11446  cjsub  11452  resqrexlemfp1  11569  resqrexlemgt0  11580  sqabsadd  11615  sqabssub  11616  abs2dif2  11667  cau3lem  11674  icodiamlt  11740  xrmaxaddlem  11820  clim  11841  clim2  11843  clim2c  11844  clim0c  11846  2clim  11861  climabs0  11867  climcn1  11868  climcn2  11869  climsqz  11895  climsqz2  11896  climub  11904  climserle  11905  fsum3cvg  11938  fisumss  11952  fsum3ser  11957  sumsplitdc  11992  fsump1i  11993  fsumlessfi  12020  telfsumo  12026  fsumparts  12030  iserabs  12035  binomlem  12043  isumsplit  12051  isum1p  12052  isumlessdc  12056  mertenslem2  12096  mertensabs  12097  prodfap0  12105  prodfrecap  12106  prodfdivap  12107  fproddccvg  12132  prodmodclem2  12137  fprodssdc  12150  fprodabs  12176  fprodeq0  12177  fprodeq0g  12198  ege2le3  12231  efsub  12241  efexp  12242  efsep  12251  sinsub  12300  cossub  12301  demoivre  12333  eirraplem  12337  moddvds  12359  0dvds  12371  iddvdsexp  12375  dvdssub  12398  dvdsle  12404  dvdsleabs  12405  dvdseq  12408  dvdsflip  12411  mulsucdiv2z  12445  divalgb  12485  divalg2  12486  ndvdsadd  12491  bitsp1  12511  gcdneg  12552  gcdabs2  12560  modgcd  12561  bezoutlemsup  12579  gcdmultiplez  12591  gcdeq  12593  dvdssq  12601  lcmcllem  12638  lcmneg  12645  lcmdvds  12650  qredeu  12668  cncongrcoprm  12677  isprm3  12689  prmrp  12716  divnumden  12767  phiprmpw  12793  crth  12795  hashgcdlem  12809  hashgcdeq  12811  modprminv  12821  modprminveq  12822  modprmn0modprm0  12828  coprimeprodsq2  12830  pcpre1  12864  pccl  12871  pcmul  12873  pcdiv  12874  pcqcl  12878  pcexp  12881  pcdvds  12887  pcndvds  12889  pcndvds2  12891  pcelnn  12893  pcgcd1  12900  pc2dvds  12902  pc11  12903  gzsubcl  12952  4sqlem3  12962  setsresg  13119  pwssnf1o  13380  xpsfeq  13427  submcl  13561  grpinvnzcl  13654  mulgnnass  13743  nmzsubg  13796  nmznsg  13799  resghm2b  13848  ghmnsgpreima  13855  gsumfzsnfd  13931  iscrng2  14027  subrngpropd  14229  issubrg3  14260  subrgpropd  14266  islmodd  14306  lss1d  14396  lspsncl  14405  lspsnid  14420  df2idl2  14522  2idlcpbl  14537  qusrhm  14541  gsumfzfsumlemm  14600  iunopn  14725  unopn  14728  eltg  14775  eltg2  14776  tgcl  14787  tgiun  14796  tgidm  14797  isopn3i  14858  isneip  14869  neipsm  14877  restbasg  14891  restopn2  14906  lmbrf  14938  cnclima  14946  lmss  14969  txbasval  14990  txlm  15002  psmetxrge0  15055  blininf  15147  blssps  15150  blss  15151  elmopn2  15172  bdmet  15225  metrest  15229  bl2ioo  15273  dvcjbr  15431  plyaddlem1  15470  plymullem1  15471  plyreres  15487  dvply1  15488  dvply2g  15489  efper  15530  sinperlem  15531  abssinper  15569  cxpexprp  15618  logcxp  15620  rpcxpcl  15626  rpcxproot  15637  rprelogbmulexp  15679  lgsval2lem  15738  lgssq2  15769  lgsprme0  15770  ausgrusgrben  16018  wlkepvtx  16225  bj-inex  16502  peano5set  16535  findset  16540  bj-findis  16574  nninfsellemsuc  16614  nninfself  16615  cvgcmp2nlemabs  16636  iooref1o  16638  trilpolemeq1  16644  nconstwlpolemgt0  16668