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	⊢ (𝜑 → 𝜓)
sylan.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylan.2	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
3	2	expcom 116	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	mpan9 281	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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  571  pm4.55dc  947  dfifp2dc  990  3adantl1  1180  3adantl2  1181  3adantl3  1182  syl3anl1  1322  syl3anl3  1324  syl3anl  1325  stoic3  1476  eupick  2160  csbiebt  3177  csbnestgf  3190  reuss2  3500  mpteq12  4192  otexg  4345  opelopabt  4379  sonr  4437  sotr  4438  issod  4439  so2nr  4441  so3nr  4442  ordelss  4499  onelon  4504  elrnmpt1s  5006  iota2  5341  funeu  5376  imadif  5435  fnbr  5459  feu  5548  f1ss  5578  f1ssres  5581  f1resf1  5582  dffo2  5593  foco  5600  foun  5632  fun11iun  5634  ffoss  5646  funbrfv  5712  fvco3  5747  fvopab6  5773  funfvbrb  5790  elpreima  5796  ffvelcdm  5809  ffvelcdmda  5811  dffo4  5824  fmptco  5842  fsn2  5850  fncofn  5861  fvconst2g  5897  fex  5914  funfvima  5917  f1elima  5945  f1ocnvfv1  5949  f1ocnvfv2  5950  cocan2  5960  foeqcnvco  5962  isocnv  5983  isores2  5985  isoini  5990  isoselem  5992  f1oiso  5998  f1ofveu  6037  eloprabga  6139  suppssof1  6283  ofco  6284  offveqb  6285  ofc1g  6287  ofc2g  6288  caofid0l  6292  caofid0r  6293  caofid1  6294  caofid2  6295  fnexALT  6303  f1dmex  6308  ot1stg  6345  ot2ndg  6346  ot3rdgg  6347  eqopi  6365  2ndrn  6376  fo2ndf  6422  suppval1  6438  ressuppss  6453  suppssrst  6460  suppssrgst  6461  smores3  6523  smores2  6524  smoel  6530  smoiso  6532  tfrlem1  6538  tfrlemisucaccv  6555  tfrlemibxssdm  6557  tfrlemiubacc  6560  tfr1onlemsucaccv  6571  tfr1onlembfn  6574  tfr1onlemubacc  6576  tfr1onlemaccex  6578  tfr1onlemres  6579  tfrcllemsucaccv  6584  tfrcllembfn  6587  tfrcllemubacc  6589  tfrcllemaccex  6591  tfrcllemres  6592  tfrcl  6594  frecrdg  6638  omv2  6697  nnasuc  6708  nnmsuc  6709  nnacom  6716  nnaass  6717  nnmass  6719  nntri1  6728  nndifsnid  6739  nnmordi  6748  swoer  6794  erth  6812  riinerm  6841  qliftlem  6846  ecovass  6877  ecoviass  6878  elmapssres  6906  fvixp  6937  f1domg  6996  domssr  7016  endomtr  7029  xpsnen2g  7079  enen1  7092  enen2  7093  domen1  7094  domen2  7095  mapen  7098  mapxpen  7100  ssenen  7104  phplem1  7105  fidifsnid  7125  findcard  7144  findcard2  7145  findcard2s  7146  fidcen  7155  fieq0  7262  isotilem  7296  supisolem  7298  inflbti  7314  ordiso2  7325  djuex  7333  updjudhcoinlf  7370  updjudhcoinrg  7371  updjud  7372  ctssdccl  7401  enumctlemm  7404  nnnninf  7416  finomni  7430  pm54.43  7486  acfun  7513  ccfunen  7577  cc2lem  7579  cc3  7581  addclpi  7641  addasspig  7644  mulasspig  7646  addnidpig  7650  nnppipi  7657  ltanqi  7716  ltmnqi  7717  ltexnqq  7722  archnqq  7731  prarloclemarch2  7733  enq0sym  7746  enq0tr  7748  nqnq0pi  7752  nqnq0  7755  mulcanenq0ec  7759  addclnq0  7765  nqpnq0nq  7767  distrnq0  7773  addassnq0lemcl  7775  addassnq0  7776  prubl  7800  prarloclemlt  7807  genpdf  7822  genipv  7823  genpelvl  7826  genpelvu  7827  genpml  7831  genpmu  7832  genprndl  7835  genprndu  7836  genpassl  7838  genpassu  7839  genpassg  7840  addnqprl  7843  addnqpru  7844  addlocpr  7850  nqprm  7856  nqprl  7865  nqpru  7866  mulnqprl  7882  mulnqpru  7883  mullocprlem  7884  mullocpr  7885  addcomprg  7892  mulcomprg  7894  distrlem1prl  7896  distrlem1pru  7897  distrlem4prl  7898  distrlem4pru  7899  ltprordil  7903  1idprl  7904  1idpru  7905  ltpopr  7909  ltsopr  7910  ltaddpr  7911  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  ltexprlemdisj  7920  ltexprlemloc  7921  ltexprlemfl  7923  ltexprlemrl  7924  ltexprlemfu  7925  ltexprlemru  7926  addcanprleml  7928  addcanprlemu  7929  prplnqu  7934  recexprlemloc  7945  recexprlem1ssl  7947  recexprlem1ssu  7948  recexprlemss1l  7949  recexprlemss1u  7950  aptiprleml  7953  aptiprlemu  7954  cauappcvgprlemloc  7966  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  caucvgprlemloc  7989  caucvgprlemladdrl  7992  caucvgprprlemml  8008  caucvgprprlemloc  8017  00sr  8083  map2psrprg  8119  suplocsrlempr  8121  suplocsrlem  8122  adddir  8264  axsuploc  8345  eqle  8364  le2tri3i  8381  mul4  8404  muladd11  8405  cnegexlem3  8449  addsub12  8485  2addsub  8486  addsubeq4  8487  subadd4  8516  negcon1  8524  negdi2  8530  negsubdi2  8531  neg2sub  8532  renegcl  8533  muladd  8656  subdir  8658  gt0ne0  8700  ltnegcon1  8736  lenegcon1  8739  eqord1  8756  eqord2  8757  recexre  8851  ltmul1  8865  recexap  8926  div12ap  8967  rerecapb  9116  p1le  9122  ltmul2  9129  gt0div  9143  ge0div  9144  zlem1lt  9633  nnaddm1cl  9638  zdceq  9652  gtndiv  9672  prime  9676  msqznn  9677  btwnz  9696  uzss  9874  eluzadd  9882  nn0pzuz  9918  supinfneg  9926  infsupneg  9927  divfnzn  9952  qnegcl  9967  qreccl  9973  elpqb  9981  xaddass  10201  xleadd1a  10205  xlesubadd  10215  elico2  10269  iccss  10273  iccsupr  10298  elfz5  10350  fznn  10422  difelfznle  10468  fzoaddel  10531  elincfzoext  10537  qdceq  10603  qbtwnxr  10616  flqbi2  10650  adddivflid  10651  fldivnn0  10654  divfl0  10655  flqmulnn0  10658  fldivnn0le  10662  fldiv4p1lem1div2  10664  ceiqle  10674  flqdiv  10682  modqmulnn  10703  frecuzrdgtcl  10773  frecuzrdgsuc  10775  frecuzrdgdomlem  10778  frecuzrdgfunlem  10780  frecuzrdgsuctlem  10784  seqm1g  10835  seq3caopr2  10854  seqcaopr2g  10855  iseqf1olemkle  10858  seq3f1olemp  10876  seqf1oglem2  10881  seqf1og  10882  seq3id  10886  seq3z  10889  expap0  10930  mulexp  10939  mulexpzap  10940  expmul  10945  leexp1a  10955  expubnd  10957  zesq  11019  bernneq  11021  bernneq3  11023  modqexp  11027  facdiv  11099  facndiv  11100  faclbnd3  11104  faclbnd6  11105  bccmpl  11115  bcpasc  11127  bccl  11128  hashfibclem  11202  hashfibc  11203  seq3coll  11210  fundm2domnop  11217  wrdsymb1  11257  ccatfv0  11287  ccatrn  11293  ccat2s1cl  11317  lswccats1fst  11328  swrdspsleq  11355  pfxtrcfv  11381  pfxsuffeqwrdeq  11386  pfxlswccat  11401  wrdeqs1cat  11408  cats1un  11409  swrdccatin1  11413  pfxccatin12lem4  11414  swrdccatin2  11417  pfxccatin12  11421  swrdccat  11423  shftlem  11497  ovshftex  11500  shftval4  11509  shftf  11511  shftcan2  11516  crim  11539  mulreap  11545  remul2  11554  immul2  11561  cjexp  11574  caucvgre  11662  r19.2uz  11674  sqrtsq2  11724  absnid  11754  absexp  11760  nn0abscl  11766  abslt  11769  lenegsq  11776  cau3lem  11795  minmax  11911  xrmaxadd  11942  clim  11962  climshftlemg  11983  climcn1  11989  climcn1lem  12000  clim2ser  12018  clim2ser2  12019  iserex  12020  isermulc2  12021  climub  12025  climcaucn  12032  serf0  12033  summodclem3  12062  summodclem2a  12063  summodclem2  12064  summodc  12065  fsum3  12069  fsumf1o  12072  fisumss  12074  isumss2  12075  fsumcl2lem  12080  fsumadd  12088  fsumsplit  12089  isummulc2  12108  fsum2d  12117  fsummulc2  12130  telfsumo  12148  fsumparts  12152  hash2iun1dif1  12162  bcxmas  12171  isumshft  12172  isumsplit  12173  expcnvap0  12184  geolim  12193  geolim2  12194  cvgratnnlemmn  12207  cvgratnnlemseq  12208  mertenslemi1  12217  mertenslem2  12218  mertensabs  12219  clim2divap  12222  prodmodclem3  12257  prodmodclem2a  12258  fprodseq  12265  fprodf1o  12270  fprodmul  12273  fprodsplitdc  12278  efcllemp  12340  reefcl  12350  efcj  12355  efaddlem  12356  efexp  12364  reeftlcl  12371  eftlub  12372  efsep  12373  effsumlt  12374  eflegeo  12383  retanclap  12404  demoivre  12455  demoivreALT  12456  eirraplem  12459  dvdsval3  12473  p1modz1  12476  iddvdsexp  12497  alzdvds  12536  addmodlteqALT  12541  nnehalf  12586  nno  12588  ndvdsadd  12613  bitsp1e  12634  bitsp1o  12635  bitsinv1  12644  divgcdnnr  12668  neggcd  12675  gcdabs  12680  bezoutlemmain  12690  bezoutlemaz  12695  bezoutlembz  12696  gcdmultiplez  12713  gcdzeq  12714  dvdssq  12723  nninfctlemfo  12732  algrf  12738  algcvg  12741  algcvga  12744  algfx  12745  eucalgf  12748  eucalgcvga  12751  neglcm  12768  lcmabs  12769  lcmdvds  12772  lcmgcdeq  12776  qredeq  12789  isprm3  12811  coprm  12837  prmrp  12838  isprm6  12840  prmdvdsexpb  12842  rpexp  12846  cncongrprm  12850  sqrt2irraplemnn  12872  phibndlem  12909  phiprmpw  12915  eulerthlemh  12924  eulerthlemth  12925  fermltl  12927  prmdivdiv  12930  modprm1div  12941  m1dvdsndvds  12942  coprimeprodsq  12951  pczpre  12991  pczcl  12992  pcexp  13003  pczdvds  13008  pczndvds  13010  pczndvds2  13012  pcdvdsb  13014  pcneg  13019  pcprmpw  13028  difsqpwdvds  13032  pcmptcl  13036  pcprod  13040  fldivp1  13042  infpnlem2  13054  1arithlem4  13060  ennnfonelemrn  13162  topnidg  13457  pwselbasb  13498  pwsplusgval  13500  pwsmulrval  13501  imasaddfnlemg  13519  imasaddflemg  13521  qusin  13531  mgmlrid  13584  mndass  13629  prdsidlem  13652  mhmco  13695  gsumsubm  13699  gsumwcl  13702  gsumwmhm  13703  grpass  13714  grpinvex  13715  dfgrp2  13732  grplid  13736  grprid  13737  grprcan  13742  grpinvssd  13782  grpinvval2  13788  prdsinvlem  13813  pwsinvg  13817  mhmid  13824  mhmmnd  13825  ghmgrp  13827  mulgnn  13835  mulgnnp1  13839  mulgnegnn  13841  mulgnnsubcl  13843  mulgz  13859  issubg2m  13898  issubg4m  13902  subgintm  13907  nmzbi  13918  eqger  13933  eqgid  13935  eqgen  13936  qusgrp  13941  qusadd  13943  qusinv  13945  qussub  13946  ghminv  13959  ghmsub  13960  ghmrn  13966  resghm2b  13971  ghmf1  13982  conjsubg  13986  conjsubgen  13987  qusghm  13991  cmncom  14011  ablsubadd  14021  ablsubsub23  14034  ghmcmn  14036  gsumfzreidx  14046  mgpress  14067  srg1expzeq1  14131  ringinvnz1ne0  14185  ringinvnzdiv  14186  dvdsrd  14231  dvdsunit  14249  unitinvcl  14260  unitinvinv  14261  unitlinv  14263  unitrinv  14264  rhmunitinv  14315  subrngintm  14349  subrg1  14368  subrguss  14373  subrginv  14374  subrgunit  14376  subrgugrp  14377  subrgintm  14380  resrhm  14385  resrhm2b  14386  lmodass  14443  lmodlcan  14444  lmod0vlid  14458  lmod0vrid  14459  lmod0vid  14460  lmodvs0  14462  lcomf  14467  lmodvnegcl  14468  lmodvnegid  14469  lmodvsubadd  14478  lmodsubid  14487  lss1d  14523  lspval  14530  lspsnel6  14548  lspsnneg  14560  sralmod  14590  dflidl2rng  14621  lidlacl  14624  dflidl2  14628  df2idl2  14649  qusmul2  14669  quscrng  14673  cnfldmulg  14716  znf1o  14791  znidom  14797  psraddcl  14827  psr0lid  14829  tgss3  14935  clsval  14968  clsss3  14987  neiss2  14999  resttop  15027  resttopon2  15035  lmconst  15073  cnima  15077  cnntri  15081  cncnp  15087  cnrest  15092  cndis  15098  lmss  15103  lmff  15106  lmtopcnp  15107  txcnp  15128  upxp  15129  uptx  15131  cnmpt11  15140  hmeoima  15167  hmeoopn  15168  hmeocld  15169  hmeontr  15170  hmeoimaf1o  15171  mettri2  15219  met0  15221  metres2  15238  blpnf  15257  xblss2ps  15261  xblss2  15262  blbas  15290  blres  15291  xmetec  15294  mopnss  15307  xmstri2  15327  mstri2  15328  xmstri  15329  mstri  15330  xmstri3  15331  mstri3  15332  msrtri  15333  mopni3  15341  unimopn  15343  comet  15356  bdxmet  15358  climcncf  15441  dedekindeulemuub  15474  dedekindicclemuub  15483  ivthdichlem  15508  dvfgg  15545  dvidlemap  15548  dvidrelem  15549  dvidsslem  15550  dvfre  15567  dvmptfsum  15582  plyadd  15608  plymul  15609  reeff1olem  15628  reeff1o  15630  sinperlem  15665  abssinper  15703  reexplog  15728  relogexp  15729  cxpexpnn  15753  cxprec  15767  rpcxpmul2  15770  abscxp  15772  wilthlem1  15840  sgmval2  15844  sgmnncl  15848  0sgmppw  15853  perfectlem1  15859  lgsdir  15900  lgsprme0  15907  lgsdinn0  15913  gausslemma2dlem3  15928  gausslemma2dlem5a  15930  2lgslem1a2  15952  2lgslem1a  15953  2lgslem3  15966  2lgs  15969  umgredgprv  16102  umgrislfupgrdom  16118  uspgredgiedg  16165  uspgriedgedg  16166  usgrislfuspgrdom  16177  usgredg2en  16182  usgredgprv  16183  usgrpredgv  16185  usgredg  16187  usgrnloopv  16188  usgredgne  16191  usgredg3  16201  usgredgedg  16214  usgredgdomord  16217  usgr1vr  16235  subgruhgrfun  16255  subupgr  16260  subumgr  16261  subusgr  16262  umgrwlknloop  16355  wlkres  16366  clwwlkccatlem  16387  clwwlkccat  16388  depindlem1  16493  depindlem2  16494  depindlem3  16495  bj-inex  16669  bj-nn0suc  16726  bj-nn0sucALT  16740  trilpolemeq1  16816  trilpolemlt1  16817  trirec0  16820  nconstwlpolemgt0  16841