Theorem sylan 277

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 114	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	mpan9 275	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  sylanb  278  sylanbr  279  syl2an  283  sylanl1  394  sylanl2  395  mpanl1  425  mpanl2  426  adantll  460  adantlr  461  ancom1s  534  3adantl1  1097  3adantl2  1098  3adantl3  1099  syl3anl1  1220  syl3anl3  1222  syl3anl  1223  stoic3  1363  eupick  2024  csbiebt  2956  csbnestgf  2969  reuss2  3268  mpteq12  3898  otexg  4033  opelopabt  4065  sonr  4120  sotr  4121  issod  4122  so2nr  4124  so3nr  4125  ordelss  4182  onelon  4187  elrnmpt1s  4655  iota2  4974  funeu  5007  imadif  5061  fnbr  5083  feu  5158  f1ss  5187  f1ssres  5190  f1resf1  5191  dffo2  5202  foco  5208  foun  5237  fun11iun  5239  ffoss  5250  funbrfv  5308  fvco3  5340  fvopab6  5361  funfvbrb  5377  elpreima  5383  ffvelrn  5397  ffvelrnda  5399  dffo4  5412  fmptco  5429  fsn2  5436  fvconst2g  5474  fex  5487  funfvima  5489  foelrnOLD  5495  f1elima  5515  f1ocnvfv1  5519  f1ocnvfv2  5520  cocan2  5530  foeqcnvco  5532  isocnv  5553  isores2  5555  isoini  5560  isoselem  5562  f1oiso  5568  f1ofveu  5603  eloprabga  5694  grprinvlem  5798  suppssof1  5831  ofco  5832  offveqb  5833  fnexALT  5843  f1dmex  5846  ot1stg  5882  ot2ndg  5883  ot3rdgg  5884  eqopi  5901  2ndrn  5912  fo2ndf  5951  smores3  6014  smores2  6015  smoel  6021  smoiso  6023  tfrlem1  6029  tfrlemisucaccv  6046  tfrlemibxssdm  6048  tfrlemiubacc  6051  tfr1onlemsucaccv  6062  tfr1onlembfn  6065  tfr1onlemubacc  6067  tfr1onlemaccex  6069  tfr1onlemres  6070  tfrcllemsucaccv  6075  tfrcllembfn  6078  tfrcllemubacc  6080  tfrcllemaccex  6082  tfrcllemres  6083  tfrcl  6085  frecrdg  6129  omv2  6182  nnasuc  6193  nnmsuc  6194  nnacom  6201  nnaass  6202  nnmass  6204  nntri1  6213  nndifsnid  6220  nnmordi  6229  swoer  6274  erth  6290  riinerm  6319  qliftlem  6324  ecovass  6355  ecoviass  6356  elmapssres  6384  f1domg  6429  endomtr  6461  xpsnen2g  6499  enen1  6510  enen2  6511  domen1  6512  domen2  6513  mapen  6516  mapxpen  6518  ssenen  6521  phplem1  6522  fidifsnid  6541  findcard  6558  findcard2  6559  findcard2s  6560  isotilem  6648  supisolem  6650  inflbti  6666  ordiso2  6675  djuex  6683  updjudhcoinlf  6718  updjudhcoinrg  6719  updjud  6720  finomni  6743  nnnninf  6753  pm54.43  6765  addclpi  6833  addasspig  6836  mulasspig  6838  addnidpig  6842  nnppipi  6849  ltanqi  6908  ltmnqi  6909  ltexnqq  6914  archnqq  6923  prarloclemarch2  6925  enq0sym  6938  enq0tr  6940  nqnq0pi  6944  nqnq0  6947  mulcanenq0ec  6951  addclnq0  6957  nqpnq0nq  6959  distrnq0  6965  addassnq0lemcl  6967  addassnq0  6968  prubl  6992  prarloclemlt  6999  genpdf  7014  genipv  7015  genpelvl  7018  genpelvu  7019  genpml  7023  genpmu  7024  genprndl  7027  genprndu  7028  genpassl  7030  genpassu  7031  genpassg  7032  addnqprl  7035  addnqpru  7036  addlocpr  7042  nqprm  7048  nqprl  7057  nqpru  7058  mulnqprl  7074  mulnqpru  7075  mullocprlem  7076  mullocpr  7077  addcomprg  7084  mulcomprg  7086  distrlem1prl  7088  distrlem1pru  7089  distrlem4prl  7090  distrlem4pru  7091  ltprordil  7095  1idprl  7096  1idpru  7097  ltpopr  7101  ltsopr  7102  ltaddpr  7103  ltexprlemm  7106  ltexprlemopl  7107  ltexprlemlol  7108  ltexprlemopu  7109  ltexprlemupu  7110  ltexprlemdisj  7112  ltexprlemloc  7113  ltexprlemfl  7115  ltexprlemrl  7116  ltexprlemfu  7117  ltexprlemru  7118  addcanprleml  7120  addcanprlemu  7121  prplnqu  7126  recexprlemloc  7137  recexprlem1ssl  7139  recexprlem1ssu  7140  recexprlemss1l  7141  recexprlemss1u  7142  aptiprleml  7145  aptiprlemu  7146  cauappcvgprlemloc  7158  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgprlemloc  7181  caucvgprlemladdrl  7184  caucvgprprlemml  7200  caucvgprprlemloc  7209  00sr  7262  adddir  7426  eqle  7523  le2tri3i  7540  mul4  7561  muladd11  7562  cnegexlem3  7606  addsub12  7642  2addsub  7643  addsubeq4  7644  subadd4  7673  negcon1  7681  negdi2  7687  negsubdi2  7688  neg2sub  7689  renegcl  7690  muladd  7809  subdir  7811  gt0ne0  7852  ltnegcon1  7888  lenegcon1  7891  recexre  7999  ltmul1  8013  recexap  8064  div12ap  8103  p1le  8248  ltmul2  8255  gt0div  8269  ge0div  8270  zlem1lt  8742  nnaddm1cl  8747  zdceq  8758  gtndiv  8777  prime  8781  msqznn  8782  btwnz  8801  uzss  8974  eluzadd  8982  nn0pzuz  9010  supinfneg  9018  infsupneg  9019  divfnzn  9041  qnegcl  9056  qreccl  9062  elico2  9290  iccss  9294  iccsupr  9319  elfz5  9367  fznn  9436  difelfznle  9477  fzoaddel  9534  qdceq  9589  qbtwnxr  9600  flqbi2  9629  adddivflid  9630  fldivnn0  9633  divfl0  9634  flqmulnn0  9637  fldivnn0le  9641  fldiv4p1lem1div2  9643  ceiqle  9651  flqdiv  9659  modqmulnn  9680  frecuzrdgtcl  9750  frecuzrdgsuc  9752  frecuzrdgdomlem  9755  frecuzrdgfunlem  9757  frecuzrdgsuctlem  9761  iseqsplit  9816  iseqcaopr2  9819  iseqf1olemkle  9821  iseqf1olemp  9839  iseqid  9846  iseqz  9849  expap0  9887  mulexp  9896  mulexpzap  9897  expmul  9902  leexp1a  9912  expubnd  9914  zesq  9972  bernneq  9974  bernneq3  9976  facdiv  10046  facndiv  10047  faclbnd3  10051  faclbnd6  10052  bccmpl  10062  bcpasc  10074  bccl  10075  iseqcoll  10147  shftlem  10150  ovshftex  10153  shftval4  10162  shftf  10164  shftcan2  10169  crim  10191  mulreap  10197  remul2  10206  immul2  10213  cjexp  10226  caucvgre  10313  r19.2uz  10325  sqrtsq2  10375  absnid  10405  absexp  10411  nn0abscl  10417  abslt  10420  lenegsq  10427  cau3lem  10446  minmax  10559  clim  10567  climshftlemg  10588  climcn1  10594  climcn1lem  10604  clim2iser  10622  clim2iser2  10623  iiserex  10624  iisermulc2  10625  climub  10629  climcaucn  10635  serif0  10636  isummolem3  10664  isummolem2a  10665  isummolem2  10666  isummo  10667  fisum  10670  fsumf1o  10673  fisumss  10675  isumss2  10676  fsumcl2lem  10680  fsumadd  10688  fsumsplit  10689  dvdsval3  10706  iddvdsexp  10726  alzdvds  10761  addmodlteqALT  10766  nnehalf  10810  nno  10812  ndvdsadd  10837  divgcdnnr  10873  neggcd  10880  gcdabs  10885  bezoutlemmain  10893  bezoutlemaz  10898  bezoutlembz  10899  gcdmultiplez  10916  gcdzeq  10917  dvdssq  10926  ialgcvg  10936  ialgcvga  10939  ialgfx  10940  eucalgf  10943  eucialgcvga  10946  neglcm  10963  lcmabs  10964  lcmdvds  10967  lcmgcdeq  10971  qredeq  10984  isprm3  11006  coprm  11029  prmrp  11030  isprm6  11032  prmdvdsexpb  11034  rpexp  11038  cncongrprm  11042  sqrt2irraplemnn  11063  phibndlem  11098  phiprmpw  11104  bj-inex  11267  bj-nn0suc  11328  bj-nn0sucALT  11342