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  1142  3adantl2  1143  3adantl3  1144  syl3anl1  1275  syl3anl3  1277  syl3anl  1278  stoic3  1418  eupick  2092  csbiebt  3079  csbnestgf  3092  reuss2  3397  mpteq12  4059  otexg  4202  opelopabt  4234  sonr  4289  sotr  4290  issod  4291  so2nr  4293  so3nr  4294  ordelss  4351  onelon  4356  elrnmpt1s  4848  iota2  5173  funeu  5207  imadif  5262  fnbr  5284  feu  5364  f1ss  5393  f1ssres  5396  f1resf1  5397  dffo2  5408  foco  5414  foun  5445  fun11iun  5447  ffoss  5458  funbrfv  5519  fvco3  5551  fvopab6  5576  funfvbrb  5592  elpreima  5598  ffvelrn  5612  ffvelrnda  5614  dffo4  5627  fmptco  5645  fsn2  5653  fvconst2g  5693  fex  5708  funfvima  5710  f1elima  5735  f1ocnvfv1  5739  f1ocnvfv2  5740  cocan2  5750  foeqcnvco  5752  isocnv  5773  isores2  5775  isoini  5780  isoselem  5782  f1oiso  5788  f1ofveu  5824  eloprabga  5920  grprinvlem  6027  suppssof1  6061  ofco  6062  offveqb  6063  fnexALT  6073  f1dmex  6076  ot1stg  6112  ot2ndg  6113  ot3rdgg  6114  eqopi  6132  2ndrn  6143  fo2ndf  6186  smores3  6252  smores2  6253  smoel  6259  smoiso  6261  tfrlem1  6267  tfrlemisucaccv  6284  tfrlemibxssdm  6286  tfrlemiubacc  6289  tfr1onlemsucaccv  6300  tfr1onlembfn  6303  tfr1onlemubacc  6305  tfr1onlemaccex  6307  tfr1onlemres  6308  tfrcllemsucaccv  6313  tfrcllembfn  6316  tfrcllemubacc  6318  tfrcllemaccex  6320  tfrcllemres  6321  tfrcl  6323  frecrdg  6367  omv2  6424  nnasuc  6435  nnmsuc  6436  nnacom  6443  nnaass  6444  nnmass  6446  nntri1  6455  nndifsnid  6466  nnmordi  6475  swoer  6520  erth  6536  riinerm  6565  qliftlem  6570  ecovass  6601  ecoviass  6602  elmapssres  6630  fvixp  6660  f1domg  6715  endomtr  6747  xpsnen2g  6786  enen1  6797  enen2  6798  domen1  6799  domen2  6800  mapen  6803  mapxpen  6805  ssenen  6808  phplem1  6809  fidifsnid  6828  findcard  6845  findcard2  6846  findcard2s  6847  fieq0  6932  isotilem  6962  supisolem  6964  inflbti  6980  ordiso2  6991  djuex  6999  updjudhcoinlf  7036  updjudhcoinrg  7037  updjud  7038  ctssdccl  7067  enumctlemm  7070  nnnninf  7081  finomni  7095  pm54.43  7137  acfun  7154  ccfunen  7196  cc2lem  7198  cc3  7200  addclpi  7259  addasspig  7262  mulasspig  7264  addnidpig  7268  nnppipi  7275  ltanqi  7334  ltmnqi  7335  ltexnqq  7340  archnqq  7349  prarloclemarch2  7351  enq0sym  7364  enq0tr  7366  nqnq0pi  7370  nqnq0  7373  mulcanenq0ec  7377  addclnq0  7383  nqpnq0nq  7385  distrnq0  7391  addassnq0lemcl  7393  addassnq0  7394  prubl  7418  prarloclemlt  7425  genpdf  7440  genipv  7441  genpelvl  7444  genpelvu  7445  genpml  7449  genpmu  7450  genprndl  7453  genprndu  7454  genpassl  7456  genpassu  7457  genpassg  7458  addnqprl  7461  addnqpru  7462  addlocpr  7468  nqprm  7474  nqprl  7483  nqpru  7484  mulnqprl  7500  mulnqpru  7501  mullocprlem  7502  mullocpr  7503  addcomprg  7510  mulcomprg  7512  distrlem1prl  7514  distrlem1pru  7515  distrlem4prl  7516  distrlem4pru  7517  ltprordil  7521  1idprl  7522  1idpru  7523  ltpopr  7527  ltsopr  7528  ltaddpr  7529  ltexprlemm  7532  ltexprlemopl  7533  ltexprlemlol  7534  ltexprlemopu  7535  ltexprlemupu  7536  ltexprlemdisj  7538  ltexprlemloc  7539  ltexprlemfl  7541  ltexprlemrl  7542  ltexprlemfu  7543  ltexprlemru  7544  addcanprleml  7546  addcanprlemu  7547  prplnqu  7552  recexprlemloc  7563  recexprlem1ssl  7565  recexprlem1ssu  7566  recexprlemss1l  7567  recexprlemss1u  7568  aptiprleml  7571  aptiprlemu  7572  cauappcvgprlemloc  7584  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  caucvgprlemloc  7607  caucvgprlemladdrl  7610  caucvgprprlemml  7626  caucvgprprlemloc  7635  00sr  7701  map2psrprg  7737  suplocsrlempr  7739  suplocsrlem  7740  adddir  7881  axsuploc  7962  eqle  7981  le2tri3i  7998  mul4  8021  muladd11  8022  cnegexlem3  8066  addsub12  8102  2addsub  8103  addsubeq4  8104  subadd4  8133  negcon1  8141  negdi2  8147  negsubdi2  8148  neg2sub  8149  renegcl  8150  muladd  8273  subdir  8275  gt0ne0  8316  ltnegcon1  8352  lenegcon1  8355  eqord1  8372  eqord2  8373  recexre  8467  ltmul1  8481  recexap  8541  div12ap  8581  p1le  8735  ltmul2  8742  gt0div  8756  ge0div  8757  zlem1lt  9238  nnaddm1cl  9243  zdceq  9257  gtndiv  9277  prime  9281  msqznn  9282  btwnz  9301  uzss  9477  eluzadd  9485  nn0pzuz  9516  supinfneg  9524  infsupneg  9525  divfnzn  9550  qnegcl  9565  qreccl  9571  elpqb  9578  xaddass  9796  xleadd1a  9800  xlesubadd  9810  elico2  9864  iccss  9868  iccsupr  9893  elfz5  9943  fznn  10014  difelfznle  10060  fzoaddel  10117  qdceq  10172  qbtwnxr  10183  flqbi2  10216  adddivflid  10217  fldivnn0  10220  divfl0  10221  flqmulnn0  10224  fldivnn0le  10228  fldiv4p1lem1div2  10230  ceiqle  10238  flqdiv  10246  modqmulnn  10267  frecuzrdgtcl  10337  frecuzrdgsuc  10339  frecuzrdgdomlem  10342  frecuzrdgfunlem  10344  frecuzrdgsuctlem  10348  seq3caopr2  10407  iseqf1olemkle  10409  seq3f1olemp  10427  seq3id  10433  seq3z  10436  expap0  10475  mulexp  10484  mulexpzap  10485  expmul  10490  leexp1a  10500  expubnd  10502  zesq  10562  bernneq  10564  bernneq3  10566  modqexp  10570  facdiv  10640  facndiv  10641  faclbnd3  10645  faclbnd6  10646  bccmpl  10656  bcpasc  10668  bccl  10669  seq3coll  10741  shftlem  10744  ovshftex  10747  shftval4  10756  shftf  10758  shftcan2  10763  crim  10786  mulreap  10792  remul2  10801  immul2  10808  cjexp  10821  caucvgre  10909  r19.2uz  10921  sqrtsq2  10971  absnid  11001  absexp  11007  nn0abscl  11013  abslt  11016  lenegsq  11023  cau3lem  11042  minmax  11157  xrmaxadd  11188  clim  11208  climshftlemg  11229  climcn1  11235  climcn1lem  11246  clim2ser  11264  clim2ser2  11265  iserex  11266  isermulc2  11267  climub  11271  climcaucn  11278  serf0  11279  summodclem3  11307  summodclem2a  11308  summodclem2  11309  summodc  11310  fsum3  11314  fsumf1o  11317  fisumss  11319  isumss2  11320  fsumcl2lem  11325  fsumadd  11333  fsumsplit  11334  isummulc2  11353  fsum2d  11362  fsummulc2  11375  telfsumo  11393  fsumparts  11397  hash2iun1dif1  11407  bcxmas  11416  isumshft  11417  isumsplit  11418  expcnvap0  11429  geolim  11438  geolim2  11439  cvgratnnlemmn  11452  cvgratnnlemseq  11453  mertenslemi1  11462  mertenslem2  11463  mertensabs  11464  clim2divap  11467  prodmodclem3  11502  prodmodclem2a  11503  fprodseq  11510  fprodf1o  11515  fprodmul  11518  fprodsplitdc  11523  efcllemp  11585  reefcl  11595  efcj  11600  efaddlem  11601  efexp  11609  reeftlcl  11616  eftlub  11617  efsep  11618  effsumlt  11619  eflegeo  11628  retanclap  11649  demoivre  11699  demoivreALT  11700  eirraplem  11703  dvdsval3  11717  p1modz1  11720  iddvdsexp  11741  alzdvds  11777  addmodlteqALT  11782  nnehalf  11826  nno  11828  ndvdsadd  11853  divgcdnnr  11894  neggcd  11901  gcdabs  11906  bezoutlemmain  11916  bezoutlemaz  11921  bezoutlembz  11922  gcdmultiplez  11939  gcdzeq  11940  dvdssq  11949  algrf  11956  algcvg  11959  algcvga  11962  algfx  11963  eucalgf  11966  eucalgcvga  11969  neglcm  11986  lcmabs  11987  lcmdvds  11990  lcmgcdeq  11994  qredeq  12007  isprm3  12029  coprm  12053  prmrp  12054  isprm6  12056  prmdvdsexpb  12058  rpexp  12062  cncongrprm  12066  sqrt2irraplemnn  12088  phibndlem  12125  phiprmpw  12131  eulerthlemh  12140  eulerthlemth  12141  fermltl  12143  prmdivdiv  12146  modprm1div  12156  m1dvdsndvds  12157  coprimeprodsq  12166  pczpre  12206  pczcl  12207  pcexp  12218  pczdvds  12222  pczndvds  12224  pczndvds2  12226  pcdvdsb  12228  pcneg  12233  pcprmpw  12242  difsqpwdvds  12246  pcmptcl  12249  pcprod  12253  fldivp1  12255  ennnfonelemrn  12289  topnidg  12505  tgss3  12619  clsval  12652  clsss3  12671  neiss2  12683  resttop  12711  resttopon2  12719  lmconst  12757  cnima  12761  cnntri  12765  cncnp  12771  cnrest  12776  cndis  12782  lmss  12787  lmff  12790  lmtopcnp  12791  txcnp  12812  upxp  12813  uptx  12815  cnmpt11  12824  hmeoima  12851  hmeoopn  12852  hmeocld  12853  hmeontr  12854  hmeoimaf1o  12855  mettri2  12903  met0  12905  metres2  12922  blpnf  12941  xblss2ps  12945  xblss2  12946  blbas  12974  blres  12975  xmetec  12978  mopnss  12991  xmstri2  13011  mstri2  13012  xmstri  13013  mstri  13014  xmstri3  13015  mstri3  13016  msrtri  13017  mopni3  13025  unimopn  13027  comet  13040  bdxmet  13042  climcncf  13112  dedekindeulemuub  13136  dedekindicclemuub  13145  dvfgg  13198  dvidlemap  13201  dvfre  13215  reeff1olem  13233  reeff1o  13235  sinperlem  13270  abssinper  13308  reexplog  13333  relogexp  13334  cxpexpnn  13358  cxprec  13372  abscxp  13376  bj-inex  13624  bj-nn0suc  13681  bj-nn0sucALT  13695  trilpolemeq1  13753  trilpolemlt1  13754  trirec0  13757  nconstwlpolemgt0  13776