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  399  sylanl2  400  mpanl1  430  mpanl2  431  adantll  467  adantlr  468  ancom1s  558  3adantl1  1137  3adantl2  1138  3adantl3  1139  syl3anl1  1264  syl3anl3  1266  syl3anl  1267  stoic3  1407  eupick  2078  csbiebt  3039  csbnestgf  3052  reuss2  3356  mpteq12  4011  otexg  4152  opelopabt  4184  sonr  4239  sotr  4240  issod  4241  so2nr  4243  so3nr  4244  ordelss  4301  onelon  4306  elrnmpt1s  4789  iota2  5114  funeu  5148  imadif  5203  fnbr  5225  feu  5305  f1ss  5334  f1ssres  5337  f1resf1  5338  dffo2  5349  foco  5355  foun  5386  fun11iun  5388  ffoss  5399  funbrfv  5460  fvco3  5492  fvopab6  5517  funfvbrb  5533  elpreima  5539  ffvelrn  5553  ffvelrnda  5555  dffo4  5568  fmptco  5586  fsn2  5594  fvconst2g  5634  fex  5647  funfvima  5649  f1elima  5674  f1ocnvfv1  5678  f1ocnvfv2  5679  cocan2  5689  foeqcnvco  5691  isocnv  5712  isores2  5714  isoini  5719  isoselem  5721  f1oiso  5727  f1ofveu  5762  eloprabga  5858  grprinvlem  5965  suppssof1  5999  ofco  6000  offveqb  6001  fnexALT  6011  f1dmex  6014  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  eqopi  6070  2ndrn  6081  fo2ndf  6124  smores3  6190  smores2  6191  smoel  6197  smoiso  6199  tfrlem1  6205  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemiubacc  6227  tfr1onlemsucaccv  6238  tfr1onlembfn  6241  tfr1onlemubacc  6243  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembfn  6254  tfrcllemubacc  6256  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  frecrdg  6305  omv2  6361  nnasuc  6372  nnmsuc  6373  nnacom  6380  nnaass  6381  nnmass  6383  nntri1  6392  nndifsnid  6403  nnmordi  6412  swoer  6457  erth  6473  riinerm  6502  qliftlem  6507  ecovass  6538  ecoviass  6539  elmapssres  6567  fvixp  6597  f1domg  6652  endomtr  6684  xpsnen2g  6723  enen1  6734  enen2  6735  domen1  6736  domen2  6737  mapen  6740  mapxpen  6742  ssenen  6745  phplem1  6746  fidifsnid  6765  findcard  6782  findcard2  6783  findcard2s  6784  fieq0  6864  isotilem  6893  supisolem  6895  inflbti  6911  ordiso2  6920  djuex  6928  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  ctssdccl  6996  enumctlemm  6999  finomni  7012  nnnninf  7023  pm54.43  7046  acfun  7063  ccfunen  7079  addclpi  7135  addasspig  7138  mulasspig  7140  addnidpig  7144  nnppipi  7151  ltanqi  7210  ltmnqi  7211  ltexnqq  7216  archnqq  7225  prarloclemarch2  7227  enq0sym  7240  enq0tr  7242  nqnq0pi  7246  nqnq0  7249  mulcanenq0ec  7253  addclnq0  7259  nqpnq0nq  7261  distrnq0  7267  addassnq0lemcl  7269  addassnq0  7270  prubl  7294  prarloclemlt  7301  genpdf  7316  genipv  7317  genpelvl  7320  genpelvu  7321  genpml  7325  genpmu  7326  genprndl  7329  genprndu  7330  genpassl  7332  genpassu  7333  genpassg  7334  addnqprl  7337  addnqpru  7338  addlocpr  7344  nqprm  7350  nqprl  7359  nqpru  7360  mulnqprl  7376  mulnqpru  7377  mullocprlem  7378  mullocpr  7379  addcomprg  7386  mulcomprg  7388  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  ltprordil  7397  1idprl  7398  1idpru  7399  ltpopr  7403  ltsopr  7404  ltaddpr  7405  ltexprlemm  7408  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  prplnqu  7428  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  aptiprleml  7447  aptiprlemu  7448  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemloc  7483  caucvgprlemladdrl  7486  caucvgprprlemml  7502  caucvgprprlemloc  7511  00sr  7577  map2psrprg  7613  suplocsrlempr  7615  suplocsrlem  7616  adddir  7757  axsuploc  7837  eqle  7855  le2tri3i  7872  mul4  7894  muladd11  7895  cnegexlem3  7939  addsub12  7975  2addsub  7976  addsubeq4  7977  subadd4  8006  negcon1  8014  negdi2  8020  negsubdi2  8021  neg2sub  8022  renegcl  8023  muladd  8146  subdir  8148  gt0ne0  8189  ltnegcon1  8225  lenegcon1  8228  eqord1  8245  eqord2  8246  recexre  8340  ltmul1  8354  recexap  8414  div12ap  8454  p1le  8607  ltmul2  8614  gt0div  8628  ge0div  8629  zlem1lt  9110  nnaddm1cl  9115  zdceq  9126  gtndiv  9146  prime  9150  msqznn  9151  btwnz  9170  uzss  9346  eluzadd  9354  nn0pzuz  9382  supinfneg  9390  infsupneg  9391  divfnzn  9413  qnegcl  9428  qreccl  9434  xaddass  9652  xleadd1a  9656  xlesubadd  9666  elico2  9720  iccss  9724  iccsupr  9749  elfz5  9798  fznn  9869  difelfznle  9912  fzoaddel  9969  qdceq  10024  qbtwnxr  10035  flqbi2  10064  adddivflid  10065  fldivnn0  10068  divfl0  10069  flqmulnn0  10072  fldivnn0le  10076  fldiv4p1lem1div2  10078  ceiqle  10086  flqdiv  10094  modqmulnn  10115  frecuzrdgtcl  10185  frecuzrdgsuc  10187  frecuzrdgdomlem  10190  frecuzrdgfunlem  10192  frecuzrdgsuctlem  10196  seq3caopr2  10255  iseqf1olemkle  10257  seq3f1olemp  10275  seq3id  10281  seq3z  10284  expap0  10323  mulexp  10332  mulexpzap  10333  expmul  10338  leexp1a  10348  expubnd  10350  zesq  10410  bernneq  10412  bernneq3  10414  facdiv  10484  facndiv  10485  faclbnd3  10489  faclbnd6  10490  bccmpl  10500  bcpasc  10512  bccl  10513  seq3coll  10585  shftlem  10588  ovshftex  10591  shftval4  10600  shftf  10602  shftcan2  10607  crim  10630  mulreap  10636  remul2  10645  immul2  10652  cjexp  10665  caucvgre  10753  r19.2uz  10765  sqrtsq2  10815  absnid  10845  absexp  10851  nn0abscl  10857  abslt  10860  lenegsq  10867  cau3lem  10886  minmax  11001  xrmaxadd  11030  clim  11050  climshftlemg  11071  climcn1  11077  climcn1lem  11088  clim2ser  11106  clim2ser2  11107  iserex  11108  isermulc2  11109  climub  11113  climcaucn  11120  serf0  11121  summodclem3  11149  summodclem2a  11150  summodclem2  11151  summodc  11152  fsum3  11156  fsumf1o  11159  fisumss  11161  isumss2  11162  fsumcl2lem  11167  fsumadd  11175  fsumsplit  11176  isummulc2  11195  fsum2d  11204  fsummulc2  11217  telfsumo  11235  fsumparts  11239  hash2iun1dif1  11249  bcxmas  11258  isumshft  11259  isumsplit  11260  expcnvap0  11271  geolim  11280  geolim2  11281  cvgratnnlemmn  11294  cvgratnnlemseq  11295  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  clim2divap  11309  prodmodclem3  11344  prodmodclem2a  11345  efcllemp  11364  reefcl  11374  efcj  11379  efaddlem  11380  efexp  11388  reeftlcl  11395  eftlub  11396  efsep  11397  effsumlt  11398  eflegeo  11408  retanclap  11429  demoivre  11479  demoivreALT  11480  eirraplem  11483  dvdsval3  11497  iddvdsexp  11517  alzdvds  11552  addmodlteqALT  11557  nnehalf  11601  nno  11603  ndvdsadd  11628  divgcdnnr  11664  neggcd  11671  gcdabs  11676  bezoutlemmain  11686  bezoutlemaz  11691  bezoutlembz  11692  gcdmultiplez  11709  gcdzeq  11710  dvdssq  11719  algrf  11726  algcvg  11729  algcvga  11732  algfx  11733  eucalgf  11736  eucalgcvga  11739  neglcm  11756  lcmabs  11757  lcmdvds  11760  lcmgcdeq  11764  qredeq  11777  isprm3  11799  coprm  11822  prmrp  11823  isprm6  11825  prmdvdsexpb  11827  rpexp  11831  cncongrprm  11835  sqrt2irraplemnn  11857  phibndlem  11892  phiprmpw  11898  ennnfonelemrn  11932  topnidg  12133  tgss3  12247  clsval  12280  clsss3  12299  neiss2  12311  resttop  12339  resttopon2  12347  lmconst  12385  cnima  12389  cnntri  12393  cncnp  12399  cnrest  12404  cndis  12410  lmss  12415  lmff  12418  lmtopcnp  12419  txcnp  12440  upxp  12441  uptx  12443  cnmpt11  12452  hmeoima  12479  hmeoopn  12480  hmeocld  12481  hmeontr  12482  hmeoimaf1o  12483  mettri2  12531  met0  12533  metres2  12550  blpnf  12569  xblss2ps  12573  xblss2  12574  blbas  12602  blres  12603  xmetec  12606  mopnss  12619  xmstri2  12639  mstri2  12640  xmstri  12641  mstri  12642  xmstri3  12643  mstri3  12644  msrtri  12645  mopni3  12653  unimopn  12655  comet  12668  bdxmet  12670  climcncf  12740  dedekindeulemuub  12764  dedekindicclemuub  12773  dvfgg  12826  dvidlemap  12829  dvfre  12843  sinperlem  12889  abssinper  12927  bj-inex  13105  bj-nn0suc  13162  bj-nn0sucALT  13176  trilpolemeq1  13233  trilpolemlt1  13234