Theorem sylan 281

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan.1	|- ( ph -> ps )
sylan.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan	|- ( ( ph /\ ch ) -> th )

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ( ph -> ps )
2		sylan.2	. . 3 |- ( ( ps /\ ch ) -> th )
3	2	expcom 115	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	mpan9 279	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanb  282  sylanbr  283  syl2an  287  sylanl1  400  sylanl2  401  mpanl1  431  mpanl2  432  adantll  468  adantlr  469  ancom1s  559  3adantl1  1143  3adantl2  1144  3adantl3  1145  syl3anl1  1276  syl3anl3  1278  syl3anl  1279  stoic3  1419  eupick  2093  csbiebt  3084  csbnestgf  3097  reuss2  3402  mpteq12  4065  otexg  4208  opelopabt  4240  sonr  4295  sotr  4296  issod  4297  so2nr  4299  so3nr  4300  ordelss  4357  onelon  4362  elrnmpt1s  4854  iota2  5179  funeu  5213  imadif  5268  fnbr  5290  feu  5370  f1ss  5399  f1ssres  5402  f1resf1  5403  dffo2  5414  foco  5420  foun  5451  fun11iun  5453  ffoss  5464  funbrfv  5525  fvco3  5557  fvopab6  5582  funfvbrb  5598  elpreima  5604  ffvelrn  5618  ffvelrnda  5620  dffo4  5633  fmptco  5651  fsn2  5659  fvconst2g  5699  fex  5714  funfvima  5716  f1elima  5741  f1ocnvfv1  5745  f1ocnvfv2  5746  cocan2  5756  foeqcnvco  5758  isocnv  5779  isores2  5781  isoini  5786  isoselem  5788  f1oiso  5794  f1ofveu  5830  eloprabga  5929  suppssof1  6067  ofco  6068  offveqb  6069  fnexALT  6079  f1dmex  6084  ot1stg  6120  ot2ndg  6121  ot3rdgg  6122  eqopi  6140  2ndrn  6151  fo2ndf  6195  smores3  6261  smores2  6262  smoel  6268  smoiso  6270  tfrlem1  6276  tfrlemisucaccv  6293  tfrlemibxssdm  6295  tfrlemiubacc  6298  tfr1onlemsucaccv  6309  tfr1onlembfn  6312  tfr1onlemubacc  6314  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllemsucaccv  6322  tfrcllembfn  6325  tfrcllemubacc  6327  tfrcllemaccex  6329  tfrcllemres  6330  tfrcl  6332  frecrdg  6376  omv2  6433  nnasuc  6444  nnmsuc  6445  nnacom  6452  nnaass  6453  nnmass  6455  nntri1  6464  nndifsnid  6475  nnmordi  6484  swoer  6529  erth  6545  riinerm  6574  qliftlem  6579  ecovass  6610  ecoviass  6611  elmapssres  6639  fvixp  6669  f1domg  6724  endomtr  6756  xpsnen2g  6795  enen1  6806  enen2  6807  domen1  6808  domen2  6809  mapen  6812  mapxpen  6814  ssenen  6817  phplem1  6818  fidifsnid  6837  findcard  6854  findcard2  6855  findcard2s  6856  fieq0  6941  isotilem  6971  supisolem  6973  inflbti  6989  ordiso2  7000  djuex  7008  updjudhcoinlf  7045  updjudhcoinrg  7046  updjud  7047  ctssdccl  7076  enumctlemm  7079  nnnninf  7090  finomni  7104  pm54.43  7146  acfun  7163  ccfunen  7205  cc2lem  7207  cc3  7209  addclpi  7268  addasspig  7271  mulasspig  7273  addnidpig  7277  nnppipi  7284  ltanqi  7343  ltmnqi  7344  ltexnqq  7349  archnqq  7358  prarloclemarch2  7360  enq0sym  7373  enq0tr  7375  nqnq0pi  7379  nqnq0  7382  mulcanenq0ec  7386  addclnq0  7392  nqpnq0nq  7394  distrnq0  7400  addassnq0lemcl  7402  addassnq0  7403  prubl  7427  prarloclemlt  7434  genpdf  7449  genipv  7450  genpelvl  7453  genpelvu  7454  genpml  7458  genpmu  7459  genprndl  7462  genprndu  7463  genpassl  7465  genpassu  7466  genpassg  7467  addnqprl  7470  addnqpru  7471  addlocpr  7477  nqprm  7483  nqprl  7492  nqpru  7493  mulnqprl  7509  mulnqpru  7510  mullocprlem  7511  mullocpr  7512  addcomprg  7519  mulcomprg  7521  distrlem1prl  7523  distrlem1pru  7524  distrlem4prl  7525  distrlem4pru  7526  ltprordil  7530  1idprl  7531  1idpru  7532  ltpopr  7536  ltsopr  7537  ltaddpr  7538  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  ltexprlemdisj  7547  ltexprlemloc  7548  ltexprlemfl  7550  ltexprlemrl  7551  ltexprlemfu  7552  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  prplnqu  7561  recexprlemloc  7572  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  recexprlemss1u  7577  aptiprleml  7580  aptiprlemu  7581  cauappcvgprlemloc  7593  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemloc  7616  caucvgprlemladdrl  7619  caucvgprprlemml  7635  caucvgprprlemloc  7644  00sr  7710  map2psrprg  7746  suplocsrlempr  7748  suplocsrlem  7749  adddir  7890  axsuploc  7971  eqle  7990  le2tri3i  8007  mul4  8030  muladd11  8031  cnegexlem3  8075  addsub12  8111  2addsub  8112  addsubeq4  8113  subadd4  8142  negcon1  8150  negdi2  8156  negsubdi2  8157  neg2sub  8158  renegcl  8159  muladd  8282  subdir  8284  gt0ne0  8325  ltnegcon1  8361  lenegcon1  8364  eqord1  8381  eqord2  8382  recexre  8476  ltmul1  8490  recexap  8550  div12ap  8590  p1le  8744  ltmul2  8751  gt0div  8765  ge0div  8766  zlem1lt  9247  nnaddm1cl  9252  zdceq  9266  gtndiv  9286  prime  9290  msqznn  9291  btwnz  9310  uzss  9486  eluzadd  9494  nn0pzuz  9525  supinfneg  9533  infsupneg  9534  divfnzn  9559  qnegcl  9574  qreccl  9580  elpqb  9587  xaddass  9805  xleadd1a  9809  xlesubadd  9819  elico2  9873  iccss  9877  iccsupr  9902  elfz5  9952  fznn  10024  difelfznle  10070  fzoaddel  10127  qdceq  10182  qbtwnxr  10193  flqbi2  10226  adddivflid  10227  fldivnn0  10230  divfl0  10231  flqmulnn0  10234  fldivnn0le  10238  fldiv4p1lem1div2  10240  ceiqle  10248  flqdiv  10256  modqmulnn  10277  frecuzrdgtcl  10347  frecuzrdgsuc  10349  frecuzrdgdomlem  10352  frecuzrdgfunlem  10354  frecuzrdgsuctlem  10358  seq3caopr2  10417  iseqf1olemkle  10419  seq3f1olemp  10437  seq3id  10443  seq3z  10446  expap0  10485  mulexp  10494  mulexpzap  10495  expmul  10500  leexp1a  10510  expubnd  10512  zesq  10573  bernneq  10575  bernneq3  10577  modqexp  10581  facdiv  10651  facndiv  10652  faclbnd3  10656  faclbnd6  10657  bccmpl  10667  bcpasc  10679  bccl  10680  seq3coll  10755  shftlem  10758  ovshftex  10761  shftval4  10770  shftf  10772  shftcan2  10777  crim  10800  mulreap  10806  remul2  10815  immul2  10822  cjexp  10835  caucvgre  10923  r19.2uz  10935  sqrtsq2  10985  absnid  11015  absexp  11021  nn0abscl  11027  abslt  11030  lenegsq  11037  cau3lem  11056  minmax  11171  xrmaxadd  11202  clim  11222  climshftlemg  11243  climcn1  11249  climcn1lem  11260  clim2ser  11278  clim2ser2  11279  iserex  11280  isermulc2  11281  climub  11285  climcaucn  11292  serf0  11293  summodclem3  11321  summodclem2a  11322  summodclem2  11323  summodc  11324  fsum3  11328  fsumf1o  11331  fisumss  11333  isumss2  11334  fsumcl2lem  11339  fsumadd  11347  fsumsplit  11348  isummulc2  11367  fsum2d  11376  fsummulc2  11389  telfsumo  11407  fsumparts  11411  hash2iun1dif1  11421  bcxmas  11430  isumshft  11431  isumsplit  11432  expcnvap0  11443  geolim  11452  geolim2  11453  cvgratnnlemmn  11466  cvgratnnlemseq  11467  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  clim2divap  11481  prodmodclem3  11516  prodmodclem2a  11517  fprodseq  11524  fprodf1o  11529  fprodmul  11532  fprodsplitdc  11537  efcllemp  11599  reefcl  11609  efcj  11614  efaddlem  11615  efexp  11623  reeftlcl  11630  eftlub  11631  efsep  11632  effsumlt  11633  eflegeo  11642  retanclap  11663  demoivre  11713  demoivreALT  11714  eirraplem  11717  dvdsval3  11731  p1modz1  11734  iddvdsexp  11755  alzdvds  11792  addmodlteqALT  11797  nnehalf  11841  nno  11843  ndvdsadd  11868  divgcdnnr  11909  neggcd  11916  gcdabs  11921  bezoutlemmain  11931  bezoutlemaz  11936  bezoutlembz  11937  gcdmultiplez  11954  gcdzeq  11955  dvdssq  11964  algrf  11977  algcvg  11980  algcvga  11983  algfx  11984  eucalgf  11987  eucalgcvga  11990  neglcm  12007  lcmabs  12008  lcmdvds  12011  lcmgcdeq  12015  qredeq  12028  isprm3  12050  coprm  12076  prmrp  12077  isprm6  12079  prmdvdsexpb  12081  rpexp  12085  cncongrprm  12089  sqrt2irraplemnn  12111  phibndlem  12148  phiprmpw  12154  eulerthlemh  12163  eulerthlemth  12164  fermltl  12166  prmdivdiv  12169  modprm1div  12179  m1dvdsndvds  12180  coprimeprodsq  12189  pczpre  12229  pczcl  12230  pcexp  12241  pczdvds  12245  pczndvds  12247  pczndvds2  12249  pcdvdsb  12251  pcneg  12256  pcprmpw  12265  difsqpwdvds  12269  pcmptcl  12272  pcprod  12276  fldivp1  12278  infpnlem2  12290  1arithlem4  12296  ennnfonelemrn  12352  topnidg  12569  mgmlrid  12610  tgss3  12718  clsval  12751  clsss3  12770  neiss2  12782  resttop  12810  resttopon2  12818  lmconst  12856  cnima  12860  cnntri  12864  cncnp  12870  cnrest  12875  cndis  12881  lmss  12886  lmff  12889  lmtopcnp  12890  txcnp  12911  upxp  12912  uptx  12914  cnmpt11  12923  hmeoima  12950  hmeoopn  12951  hmeocld  12952  hmeontr  12953  hmeoimaf1o  12954  mettri2  13002  met0  13004  metres2  13021  blpnf  13040  xblss2ps  13044  xblss2  13045  blbas  13073  blres  13074  xmetec  13077  mopnss  13090  xmstri2  13110  mstri2  13111  xmstri  13112  mstri  13113  xmstri3  13114  mstri3  13115  msrtri  13116  mopni3  13124  unimopn  13126  comet  13139  bdxmet  13141  climcncf  13211  dedekindeulemuub  13235  dedekindicclemuub  13244  dvfgg  13297  dvidlemap  13300  dvfre  13314  reeff1olem  13332  reeff1o  13334  sinperlem  13369  abssinper  13407  reexplog  13432  relogexp  13433  cxpexpnn  13457  cxprec  13471  abscxp  13475  lgsdir  13576  lgsprme0  13583  lgsdinn0  13589  bj-inex  13789  bj-nn0suc  13846  bj-nn0sucALT  13860  trilpolemeq1  13919  trilpolemlt1  13920  trirec0  13923  nconstwlpolemgt0  13942