Theorem sylan 283

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 116	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	mpan9 281	1 |- ( ( ph /\ ch ) -> 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:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  402  sylanl2  403  mpanl1  434  mpanl2  435  syldanl  449  adantll  476  adantlr  477  ancom1s  569  3adantl1  1153  3adantl2  1154  3adantl3  1155  syl3anl1  1286  syl3anl3  1288  syl3anl  1289  stoic3  1431  eupick  2105  csbiebt  3096  csbnestgf  3109  reuss2  3415  mpteq12  4086  otexg  4230  opelopabt  4262  sonr  4317  sotr  4318  issod  4319  so2nr  4321  so3nr  4322  ordelss  4379  onelon  4384  elrnmpt1s  4877  iota2  5206  funeu  5241  imadif  5296  fnbr  5318  feu  5398  f1ss  5427  f1ssres  5430  f1resf1  5431  dffo2  5442  foco  5448  foun  5480  fun11iun  5482  ffoss  5493  funbrfv  5554  fvco3  5587  fvopab6  5612  funfvbrb  5629  elpreima  5635  ffvelcdm  5649  ffvelcdmda  5651  dffo4  5664  fmptco  5682  fsn2  5690  fvconst2g  5730  fex  5745  funfvima  5748  f1elima  5773  f1ocnvfv1  5777  f1ocnvfv2  5778  cocan2  5788  foeqcnvco  5790  isocnv  5811  isores2  5813  isoini  5818  isoselem  5820  f1oiso  5826  f1ofveu  5862  eloprabga  5961  suppssof1  6099  ofco  6100  offveqb  6101  fnexALT  6111  f1dmex  6116  ot1stg  6152  ot2ndg  6153  ot3rdgg  6154  eqopi  6172  2ndrn  6183  fo2ndf  6227  smores3  6293  smores2  6294  smoel  6300  smoiso  6302  tfrlem1  6308  tfrlemisucaccv  6325  tfrlemibxssdm  6327  tfrlemiubacc  6330  tfr1onlemsucaccv  6341  tfr1onlembfn  6344  tfr1onlemubacc  6346  tfr1onlemaccex  6348  tfr1onlemres  6349  tfrcllemsucaccv  6354  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemaccex  6361  tfrcllemres  6362  tfrcl  6364  frecrdg  6408  omv2  6465  nnasuc  6476  nnmsuc  6477  nnacom  6484  nnaass  6485  nnmass  6487  nntri1  6496  nndifsnid  6507  nnmordi  6516  swoer  6562  erth  6578  riinerm  6607  qliftlem  6612  ecovass  6643  ecoviass  6644  elmapssres  6672  fvixp  6702  f1domg  6757  endomtr  6789  xpsnen2g  6828  enen1  6839  enen2  6840  domen1  6841  domen2  6842  mapen  6845  mapxpen  6847  ssenen  6850  phplem1  6851  fidifsnid  6870  findcard  6887  findcard2  6888  findcard2s  6889  fieq0  6974  isotilem  7004  supisolem  7006  inflbti  7022  ordiso2  7033  djuex  7041  updjudhcoinlf  7078  updjudhcoinrg  7079  updjud  7080  ctssdccl  7109  enumctlemm  7112  nnnninf  7123  finomni  7137  pm54.43  7188  acfun  7205  ccfunen  7262  cc2lem  7264  cc3  7266  addclpi  7325  addasspig  7328  mulasspig  7330  addnidpig  7334  nnppipi  7341  ltanqi  7400  ltmnqi  7401  ltexnqq  7406  archnqq  7415  prarloclemarch2  7417  enq0sym  7430  enq0tr  7432  nqnq0pi  7436  nqnq0  7439  mulcanenq0ec  7443  addclnq0  7449  nqpnq0nq  7451  distrnq0  7457  addassnq0lemcl  7459  addassnq0  7460  prubl  7484  prarloclemlt  7491  genpdf  7506  genipv  7507  genpelvl  7510  genpelvu  7511  genpml  7515  genpmu  7516  genprndl  7519  genprndu  7520  genpassl  7522  genpassu  7523  genpassg  7524  addnqprl  7527  addnqpru  7528  addlocpr  7534  nqprm  7540  nqprl  7549  nqpru  7550  mulnqprl  7566  mulnqpru  7567  mullocprlem  7568  mullocpr  7569  addcomprg  7576  mulcomprg  7578  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  ltprordil  7587  1idprl  7588  1idpru  7589  ltpopr  7593  ltsopr  7594  ltaddpr  7595  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  ltexprlemdisj  7604  ltexprlemloc  7605  ltexprlemfl  7607  ltexprlemrl  7608  ltexprlemfu  7609  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  prplnqu  7618  recexprlemloc  7629  recexprlem1ssl  7631  recexprlem1ssu  7632  recexprlemss1l  7633  recexprlemss1u  7634  aptiprleml  7637  aptiprlemu  7638  cauappcvgprlemloc  7650  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgprlemloc  7673  caucvgprlemladdrl  7676  caucvgprprlemml  7692  caucvgprprlemloc  7701  00sr  7767  map2psrprg  7803  suplocsrlempr  7805  suplocsrlem  7806  adddir  7947  axsuploc  8029  eqle  8048  le2tri3i  8065  mul4  8088  muladd11  8089  cnegexlem3  8133  addsub12  8169  2addsub  8170  addsubeq4  8171  subadd4  8200  negcon1  8208  negdi2  8214  negsubdi2  8215  neg2sub  8216  renegcl  8217  muladd  8340  subdir  8342  gt0ne0  8383  ltnegcon1  8419  lenegcon1  8422  eqord1  8439  eqord2  8440  recexre  8534  ltmul1  8548  recexap  8609  div12ap  8650  rerecapb  8799  p1le  8805  ltmul2  8812  gt0div  8826  ge0div  8827  zlem1lt  9308  nnaddm1cl  9313  zdceq  9327  gtndiv  9347  prime  9351  msqznn  9352  btwnz  9371  uzss  9547  eluzadd  9555  nn0pzuz  9586  supinfneg  9594  infsupneg  9595  divfnzn  9620  qnegcl  9635  qreccl  9641  elpqb  9648  xaddass  9868  xleadd1a  9872  xlesubadd  9882  elico2  9936  iccss  9940  iccsupr  9965  elfz5  10016  fznn  10088  difelfznle  10134  fzoaddel  10191  qdceq  10246  qbtwnxr  10257  flqbi2  10290  adddivflid  10291  fldivnn0  10294  divfl0  10295  flqmulnn0  10298  fldivnn0le  10302  fldiv4p1lem1div2  10304  ceiqle  10312  flqdiv  10320  modqmulnn  10341  frecuzrdgtcl  10411  frecuzrdgsuc  10413  frecuzrdgdomlem  10416  frecuzrdgfunlem  10418  frecuzrdgsuctlem  10422  seq3caopr2  10481  iseqf1olemkle  10483  seq3f1olemp  10501  seq3id  10507  seq3z  10510  expap0  10549  mulexp  10558  mulexpzap  10559  expmul  10564  leexp1a  10574  expubnd  10576  zesq  10638  bernneq  10640  bernneq3  10642  modqexp  10646  facdiv  10717  facndiv  10718  faclbnd3  10722  faclbnd6  10723  bccmpl  10733  bcpasc  10745  bccl  10746  seq3coll  10821  shftlem  10824  ovshftex  10827  shftval4  10836  shftf  10838  shftcan2  10843  crim  10866  mulreap  10872  remul2  10881  immul2  10888  cjexp  10901  caucvgre  10989  r19.2uz  11001  sqrtsq2  11051  absnid  11081  absexp  11087  nn0abscl  11093  abslt  11096  lenegsq  11103  cau3lem  11122  minmax  11237  xrmaxadd  11268  clim  11288  climshftlemg  11309  climcn1  11315  climcn1lem  11326  clim2ser  11344  clim2ser2  11345  iserex  11346  isermulc2  11347  climub  11351  climcaucn  11358  serf0  11359  summodclem3  11387  summodclem2a  11388  summodclem2  11389  summodc  11390  fsum3  11394  fsumf1o  11397  fisumss  11399  isumss2  11400  fsumcl2lem  11405  fsumadd  11413  fsumsplit  11414  isummulc2  11433  fsum2d  11442  fsummulc2  11455  telfsumo  11473  fsumparts  11477  hash2iun1dif1  11487  bcxmas  11496  isumshft  11497  isumsplit  11498  expcnvap0  11509  geolim  11518  geolim2  11519  cvgratnnlemmn  11532  cvgratnnlemseq  11533  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  clim2divap  11547  prodmodclem3  11582  prodmodclem2a  11583  fprodseq  11590  fprodf1o  11595  fprodmul  11598  fprodsplitdc  11603  efcllemp  11665  reefcl  11675  efcj  11680  efaddlem  11681  efexp  11689  reeftlcl  11696  eftlub  11697  efsep  11698  effsumlt  11699  eflegeo  11708  retanclap  11729  demoivre  11779  demoivreALT  11780  eirraplem  11783  dvdsval3  11797  p1modz1  11800  iddvdsexp  11821  alzdvds  11859  addmodlteqALT  11864  nnehalf  11908  nno  11910  ndvdsadd  11935  divgcdnnr  11976  neggcd  11983  gcdabs  11988  bezoutlemmain  11998  bezoutlemaz  12003  bezoutlembz  12004  gcdmultiplez  12021  gcdzeq  12022  dvdssq  12031  algrf  12044  algcvg  12047  algcvga  12050  algfx  12051  eucalgf  12054  eucalgcvga  12057  neglcm  12074  lcmabs  12075  lcmdvds  12078  lcmgcdeq  12082  qredeq  12095  isprm3  12117  coprm  12143  prmrp  12144  isprm6  12146  prmdvdsexpb  12148  rpexp  12152  cncongrprm  12156  sqrt2irraplemnn  12178  phibndlem  12215  phiprmpw  12221  eulerthlemh  12230  eulerthlemth  12231  fermltl  12233  prmdivdiv  12236  modprm1div  12246  m1dvdsndvds  12247  coprimeprodsq  12256  pczpre  12296  pczcl  12297  pcexp  12308  pczdvds  12312  pczndvds  12314  pczndvds2  12316  pcdvdsb  12318  pcneg  12323  pcprmpw  12332  difsqpwdvds  12336  pcmptcl  12339  pcprod  12343  fldivp1  12345  infpnlem2  12357  1arithlem4  12363  ennnfonelemrn  12419  topnidg  12700  imasaddfnlemg  12734  imasaddflemg  12736  qusin  12745  mgmlrid  12797  mndass  12824  mhmco  12873  grpass  12885  grpinvex  12886  dfgrp2  12901  grplid  12905  grprid  12906  grprcan  12909  grpinvssd  12946  grpinvval2  12952  mhmid  12978  mhmmnd  12979  ghmgrp  12981  mulgnn  12988  mulgnnp1  12990  mulgnegnn  12992  mulgnnsubcl  12994  mulgz  13009  issubg2m  13047  issubg4m  13051  subgintm  13056  nmzbi  13067  eqger  13081  eqgid  13083  eqgen  13084  cmncom  13103  ablsubadd  13113  ablsubsub23  13126  mgpress  13139  srg1expzeq1  13176  ringinvnz1ne0  13224  ringinvnzdiv  13225  dvdsrd  13261  dvdsunit  13279  unitinvcl  13290  unitinvinv  13291  unitlinv  13293  unitrinv  13294  subrg1  13350  subrguss  13355  subrginv  13356  subrgunit  13358  subrgugrp  13359  subrgintm  13362  lmodass  13391  lmodlcan  13392  lmod0vlid  13406  lmod0vrid  13407  lmod0vid  13408  cnfldmulg  13440  tgss3  13548  clsval  13581  clsss3  13600  neiss2  13612  resttop  13640  resttopon2  13648  lmconst  13686  cnima  13690  cnntri  13694  cncnp  13700  cnrest  13705  cndis  13711  lmss  13716  lmff  13719  lmtopcnp  13720  txcnp  13741  upxp  13742  uptx  13744  cnmpt11  13753  hmeoima  13780  hmeoopn  13781  hmeocld  13782  hmeontr  13783  hmeoimaf1o  13784  mettri2  13832  met0  13834  metres2  13851  blpnf  13870  xblss2ps  13874  xblss2  13875  blbas  13903  blres  13904  xmetec  13907  mopnss  13920  xmstri2  13940  mstri2  13941  xmstri  13942  mstri  13943  xmstri3  13944  mstri3  13945  msrtri  13946  mopni3  13954  unimopn  13956  comet  13969  bdxmet  13971  climcncf  14041  dedekindeulemuub  14065  dedekindicclemuub  14074  dvfgg  14127  dvidlemap  14130  dvfre  14144  reeff1olem  14162  reeff1o  14164  sinperlem  14199  abssinper  14237  reexplog  14262  relogexp  14263  cxpexpnn  14287  cxprec  14301  abscxp  14305  lgsdir  14406  lgsprme0  14413  lgsdinn0  14419  bj-inex  14629  bj-nn0suc  14686  bj-nn0sucALT  14700  trilpolemeq1  14758  trilpolemlt1  14759  trirec0  14762  nconstwlpolemgt0  14781