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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  406  sylanl2  407  mpanl1  438  mpanl2  439  syldanl  453  adantll  480  adantlr  481  ancom1s  575  pm4.55dc  951  dfifp2dc  994  3adantl1  1184  3adantl2  1185  3adantl3  1186  syl3anl1  1326  syl3anl3  1328  syl3anl  1329  stoic3  1480  eupick  2166  csbiebt  3187  csbnestgf  3200  reuss2  3513  mpteq12  4214  otexg  4370  opelopabt  4404  sonr  4462  sotr  4463  issod  4464  so2nr  4466  so3nr  4467  ordelss  4524  onelon  4529  elrnmpt1s  5032  iota2  5367  funeu  5402  imadif  5461  fnbr  5485  feu  5574  f1ss  5604  f1ssres  5607  f1resf1  5608  dffo2  5619  foco  5626  foun  5658  fun11iun  5660  ffoss  5672  funbrfv  5739  fvco3  5776  fvopab6  5805  funfvbrb  5822  elpreima  5828  ffvelcdm  5841  ffvelcdmda  5843  dffo4  5856  fmptco  5874  fsn2  5882  fncofn  5893  fvconst2g  5929  fex  5947  funfvima  5950  f1elima  5979  f1ocnvfv1  5983  f1ocnvfv2  5984  cocan2  5994  foeqcnvco  5996  isocnv  6017  isores2  6019  isoini  6024  isoselem  6026  f1oiso  6032  f1ofveu  6073  eloprabga  6175  suppssof1  6320  ofco  6321  offveqb  6322  ofc1g  6324  ofc2g  6325  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fnexALT  6340  f1dmex  6345  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  eqopi  6406  2ndrn  6417  fo2ndf  6463  suppval1  6479  ressuppss  6494  suppssrst  6501  suppssrgst  6502  smores3  6564  smores2  6565  smoel  6571  smoiso  6573  tfrlem1  6579  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemiubacc  6601  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  frecrdg  6679  omv2  6738  nnasuc  6749  nnmsuc  6750  nnacom  6757  nnaass  6758  nnmass  6760  nntri1  6769  nndifsnid  6780  nnmordi  6789  swoer  6835  erth  6853  riinerm  6882  qliftlem  6887  ecovass  6918  ecoviass  6919  elmapssres  6954  fvixp  6985  f1domg  7044  domssr  7064  endomtr  7077  xpsnen2g  7127  enen1  7140  enen2  7141  domen1  7142  domen2  7143  mapen  7146  mapxpen  7148  ssenen  7152  phplem1  7153  fidifsnid  7173  findcard  7192  findcard2  7193  findcard2s  7194  fidcen  7203  fieq0  7310  isotilem  7346  supisolem  7348  inflbti  7364  ordiso2  7375  djuex  7383  updjudhcoinlf  7420  updjudhcoinrg  7421  updjud  7422  ctssdccl  7451  enumctlemm  7454  nnnninf  7466  finomni  7480  pm54.43  7536  acfun  7563  ccfunen  7630  cc2lem  7632  cc3  7634  addclpi  7694  addasspig  7697  mulasspig  7699  addnidpig  7703  nnppipi  7710  ltanqi  7769  ltmnqi  7770  ltexnqq  7775  archnqq  7784  prarloclemarch2  7786  enq0sym  7799  enq0tr  7801  nqnq0pi  7805  nqnq0  7808  mulcanenq0ec  7812  addclnq0  7818  nqpnq0nq  7820  distrnq0  7826  addassnq0lemcl  7828  addassnq0  7829  prubl  7853  prarloclemlt  7860  genpdf  7875  genipv  7876  genpelvl  7879  genpelvu  7880  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpassl  7891  genpassu  7892  genpassg  7893  addnqprl  7896  addnqpru  7897  addlocpr  7903  nqprm  7909  nqprl  7918  nqpru  7919  mulnqprl  7935  mulnqpru  7936  mullocprlem  7937  mullocpr  7938  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  1idprl  7957  1idpru  7958  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprprlemml  8061  caucvgprprlemloc  8070  00sr  8136  map2psrprg  8172  suplocsrlempr  8174  suplocsrlem  8175  adddir  8317  axsuploc  8398  eqle  8417  le2tri3i  8434  mul4  8458  muladd11  8459  cnegexlem3  8503  addsub12  8539  2addsub  8540  addsubeq4  8541  subadd4  8570  negcon1  8578  negdi2  8584  negsubdi2  8585  neg2sub  8586  renegcl  8587  muladd  8711  subdir  8713  gt0ne0  8755  ltnegcon1  8791  lenegcon1  8794  eqord1  8811  eqord2  8812  recexre  8907  ltmul1  8921  recexap  8982  div12ap  9025  rerecapb  9174  p1le  9180  ltmul2  9187  gt0div  9201  ge0div  9202  zlem1lt  9703  nnaddm1cl  9708  zdceq  9722  gtndiv  9743  prime  9747  msqznn  9748  btwnz  9767  uzss  9945  eluzadd  9953  nn0pzuz  9989  supinfneg  9997  infsupneg  9998  divfnzn  10023  qnegcl  10038  qreccl  10044  elpqb  10052  xaddass  10273  xleadd1a  10277  xlesubadd  10287  elico2  10341  iccss  10345  iccsupr  10370  elfz5  10422  fznn  10498  difelfznle  10544  fzoaddel  10607  elincfzoext  10613  qdceq  10681  qbtwnxr  10694  flqbi2  10728  adddivflid  10729  fldivnn0  10732  divfl0  10733  flqmulnn0  10736  fldivnn0le  10740  fldiv4p1lem1div2  10742  ceiqle  10752  flqdiv  10760  modqmulnn  10781  frecuzrdgtcl  10851  frecuzrdgsuc  10853  frecuzrdgdomlem  10856  frecuzrdgfunlem  10858  frecuzrdgsuctlem  10862  seqm1g  10913  seq3caopr2  10932  seqcaopr2g  10933  iseqf1olemkle  10936  seq3f1olemp  10954  seqf1oglem2  10959  seqf1og  10960  seq3id  10964  seq3z  10967  expap0  11008  mulexp  11017  mulexpzap  11018  expmul  11023  leexp1a  11033  expubnd  11035  zesq  11098  bernneq  11100  bernneq3  11102  modqexp  11106  facdiv  11178  facndiv  11179  faclbnd3  11183  faclbnd6  11184  bccmpl  11194  bcpasc  11206  bccl  11207  hashfibclem  11284  hashfibc  11285  seq3coll  11296  fundm2domnop  11303  wrdsymb1  11343  ccatfv0  11373  ccatrn  11379  ccat2s1cl  11403  lswccats1fst  11414  swrdspsleq  11441  pfxtrcfv  11467  pfxsuffeqwrdeq  11472  pfxlswccat  11487  wrdeqs1cat  11494  cats1un  11495  swrdccatin1  11499  pfxccatin12lem4  11500  swrdccatin2  11503  pfxccatin12  11507  swrdccat  11509  shftlem  11583  ovshftex  11586  shftval4  11595  shftf  11597  shftcan2  11602  crim  11625  mulreap  11631  remul2  11640  immul2  11647  cjexp  11660  caucvgre  11749  r19.2uz  11761  sqrtsq2  11811  absnid  11841  absexp  11847  nn0abscl  11853  abslt  11856  lenegsq  11863  cau3lem  11882  minmax  11998  xrmaxadd  12029  clim  12049  climshftlemg  12070  climcn1  12076  climcn1lem  12087  clim2ser  12105  clim2ser2  12106  iserex  12107  isermulc2  12108  climub  12112  climcaucn  12119  serf0  12120  summodclem3  12149  summodclem2a  12150  summodclem2  12151  summodc  12152  fsum3  12156  fsumf1o  12159  fisumss  12161  isumss2  12162  fsumcl2lem  12167  fsumadd  12175  fsumsplit  12176  isummulc2  12195  fsum2d  12204  fsummulc2  12217  telfsumo  12235  fsumparts  12239  hash2iun1dif1  12249  bcxmas  12258  isumshft  12259  isumsplit  12260  expcnvap0  12271  geolim  12280  geolim2  12281  cvgratnnlemmn  12294  cvgratnnlemseq  12295  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  clim2divap  12309  prodmodclem3  12344  prodmodclem2a  12345  fprodseq  12352  fprodf1o  12357  fprodmul  12360  fprodsplitdc  12365  efcllemp  12427  reefcl  12437  efcj  12442  efaddlem  12443  efexp  12451  reeftlcl  12458  eftlub  12459  efsep  12460  effsumlt  12461  eflegeo  12470  retanclap  12491  demoivre  12542  demoivreALT  12543  eirraplem  12546  dvdsval3  12560  p1modz1  12563  iddvdsexp  12584  alzdvds  12623  addmodlteqALT  12628  nnehalf  12673  nno  12675  ndvdsadd  12700  bitsp1e  12721  bitsp1o  12722  bitsinv1  12731  divgcdnnr  12755  neggcd  12762  gcdabs  12767  bezoutlemmain  12777  bezoutlemaz  12782  bezoutlembz  12783  gcdmultiplez  12800  gcdzeq  12801  dvdssq  12810  nninfctlemfo  12819  algrf  12825  algcvg  12828  algcvga  12831  algfx  12832  eucalgf  12835  eucalgcvga  12838  neglcm  12855  lcmabs  12856  lcmdvds  12859  lcmgcdeq  12863  qredeq  12876  isprm3  12898  coprm  12924  prmrp  12925  isprm6  12927  prmdvdsexpb  12929  rpexp  12933  cncongrprm  12937  sqrt2irraplemnn  12959  phibndlem  12996  phiprmpw  13002  eulerthlemh  13011  eulerthlemth  13012  fermltl  13014  prmdivdiv  13017  modprm1div  13028  m1dvdsndvds  13029  coprimeprodsq  13038  pczpre  13078  pczcl  13079  pcexp  13090  pczdvds  13095  pczndvds  13097  pczndvds2  13099  pcdvdsb  13101  pcneg  13106  pcprmpw  13115  difsqpwdvds  13119  pcmptcl  13123  pcprod  13127  fldivp1  13129  infpnlem2  13141  1arithlem4  13147  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemfrcn0  13275  ennnfonelemrn  13312  topnidg  13608  imasaddfnlemg  13637  imasaddflemg  13639  qusin  13649  mgmlrid  13701  mndass  13739  mhmco  13799  gzsumwcl  13804  gzsumwmhm  13805  grpass  13816  grpinvex  13817  dfgrp2  13834  grplid  13838  grprid  13839  grprcan  13844  grpinvssd  13884  grpinvval2  13890  mhmid  13920  mhmmnd  13921  ghmgrp  13923  mulgnn  13931  mulgnnp1  13935  mulgnegnn  13937  mulgnnsubcl  13939  mulgz  13955  issubg2m  13994  issubg4m  13998  subgintm  14003  nmzbi  14014  eqger  14029  eqgid  14031  eqgen  14032  qusgrp  14037  qusadd  14039  qusinv  14041  qussub  14042  ghminv  14055  ghmsub  14056  ghmrn  14062  resghm2b  14067  ghmf1  14078  conjsubg  14082  conjsubgen  14083  qusghm  14087  cmncom  14107  ablsubadd  14118  ablsubsub23  14131  ghmcmn  14133  gzsumreidx  14143  gsumsubmfi  14170  prdsidlem  14195  prdsinvlem  14198  pwselbasb  14208  pwsplusgval  14210  pwsmulrval  14211  pwsinvg  14217  mgpress  14232  srg1expzeq1  14301  ringinvnz1ne0  14356  ringinvnzdiv  14357  dvdsrd  14403  dvdsunit  14421  unitinvcl  14432  unitinvinv  14433  unitlinv  14435  unitrinv  14436  rhmunitinv  14487  subrngintm  14522  subrg1  14541  subrguss  14546  subrginv  14547  subrgunit  14549  subrgugrp  14550  subrgintm  14553  resrhm  14558  resrhm2b  14559  lmodass  14641  lmodlcan  14642  lmod0vlid  14657  lmod0vrid  14658  lmod0vid  14659  lmodvs0  14661  lcomf  14666  lmodvnegcl  14667  lmodvnegid  14668  lmodvsubadd  14677  lmodsubid  14686  lss1d  14722  lspval  14729  ellspsn6  14747  lspsnneg  14759  sralmod  14789  dflidl2rng  14820  lidlacl  14823  dflidl2  14827  df2idl2  14848  qusmul2  14868  quscrng  14872  cnfldmulg  14915  znf1o  14988  znidom  14994  aspval  15017  asclghm  15027  issubassa2  15037  psraddcl  15073  psr0lid  15075  tgss3  15181  clsval  15214  clsss3  15233  neiss2  15245  resttop  15273  resttopon2  15281  lmconst  15319  cnima  15323  cnntri  15327  cncnp  15333  cnrest  15338  cndis  15344  lmss  15349  lmff  15352  lmtopcnp  15353  txcnp  15374  upxp  15375  uptx  15377  cnmpt11  15386  hmeoima  15413  hmeoopn  15414  hmeocld  15415  hmeontr  15416  hmeoimaf1o  15417  mettri2  15465  met0  15467  metres2  15484  blpnf  15503  xblss2ps  15507  xblss2  15508  blbas  15536  blres  15537  xmetec  15540  mopnss  15553  xmstri2  15573  mstri2  15574  xmstri  15575  mstri  15576  xmstri3  15577  mstri3  15578  msrtri  15579  mopni3  15587  unimopn  15589  comet  15602  bdxmet  15604  climcncf  15687  dedekindeulemuub  15720  dedekindicclemuub  15729  ivthdichlem  15754  dvfgg  15791  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvfre  15813  dvmptfsum  15828  plyadd  15854  plymul  15855  reeff1olem  15874  reeff1o  15876  sinperlem  15912  abssinper  15950  reexplog  15976  relogexp  15977  cxpexpnn  16004  cxprec  16018  rpcxpmul2  16021  abscxp  16023  wilthlem1  16100  sgmval2  16104  sgmnncl  16108  0sgmppw  16113  perfectlem1  16119  lgsdir  16166  lgsprme0  16173  lgsdinn0  16179  gausslemma2dlem3  16194  gausslemma2dlem5a  16196  2lgslem1a2  16218  2lgslem1a  16219  2lgslem3  16232  2lgs  16235  umgredgprv  16368  umgrislfupgrdom  16384  uspgredgiedg  16431  uspgriedgedg  16432  usgrislfuspgrdom  16443  usgredg2en  16448  usgredgprv  16449  usgrpredgv  16451  usgredg  16453  usgrnloopv  16454  usgredgne  16457  usgredg3  16467  usgredgedg  16480  usgredgdomord  16483  usgr1vr  16501  subgruhgrfun  16521  subupgr  16526  subumgr  16527  subusgr  16528  umgrwlknloop  16621  wlkres  16632  clwwlkccatlem  16653  clwwlkccat  16654  depindlem1  16759  depindlem2  16760  depindlem3  16761  bj-inex  16945  bj-nn0suc  17002  bj-nn0sucALT  17016  trilpolemeq1  17101  trilpolemlt1  17102  trirec0  17105  nconstwlpolemgt0  17126