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  569  pm4.55dc  944  dfifp2dc  987  3adantl1  1177  3adantl2  1178  3adantl3  1179  syl3anl1  1319  syl3anl3  1321  syl3anl  1322  stoic3  1473  eupick  2157  csbiebt  3164  csbnestgf  3177  reuss2  3484  mpteq12  4166  otexg  4315  opelopabt  4349  sonr  4405  sotr  4406  issod  4407  so2nr  4409  so3nr  4410  ordelss  4467  onelon  4472  elrnmpt1s  4970  iota2  5304  funeu  5339  imadif  5397  fnbr  5421  feu  5504  f1ss  5533  f1ssres  5536  f1resf1  5537  dffo2  5548  foco  5555  foun  5587  fun11iun  5589  ffoss  5600  funbrfv  5664  fvco3  5698  fvopab6  5724  funfvbrb  5741  elpreima  5747  ffvelcdm  5761  ffvelcdmda  5763  dffo4  5776  fmptco  5794  fsn2  5802  fvconst2g  5846  fex  5861  funfvima  5864  f1elima  5890  f1ocnvfv1  5894  f1ocnvfv2  5895  cocan2  5905  foeqcnvco  5907  isocnv  5928  isores2  5930  isoini  5935  isoselem  5937  f1oiso  5943  f1ofveu  5982  eloprabga  6082  suppssof1  6226  ofco  6227  offveqb  6228  ofc1g  6230  ofc2g  6231  caofid0l  6235  caofid0r  6236  caofid1  6237  caofid2  6238  fnexALT  6246  f1dmex  6251  ot1stg  6288  ot2ndg  6289  ot3rdgg  6290  eqopi  6308  2ndrn  6319  fo2ndf  6363  smores3  6429  smores2  6430  smoel  6436  smoiso  6438  tfrlem1  6444  tfrlemisucaccv  6461  tfrlemibxssdm  6463  tfrlemiubacc  6466  tfr1onlemsucaccv  6477  tfr1onlembfn  6480  tfr1onlemubacc  6482  tfr1onlemaccex  6484  tfr1onlemres  6485  tfrcllemsucaccv  6490  tfrcllembfn  6493  tfrcllemubacc  6495  tfrcllemaccex  6497  tfrcllemres  6498  tfrcl  6500  frecrdg  6544  omv2  6601  nnasuc  6612  nnmsuc  6613  nnacom  6620  nnaass  6621  nnmass  6623  nntri1  6632  nndifsnid  6643  nnmordi  6652  swoer  6698  erth  6716  riinerm  6745  qliftlem  6750  ecovass  6781  ecoviass  6782  elmapssres  6810  fvixp  6840  f1domg  6899  domssr  6919  endomtr  6932  xpsnen2g  6976  enen1  6989  enen2  6990  domen1  6991  domen2  6992  mapen  6995  mapxpen  6997  ssenen  7000  phplem1  7001  fidifsnid  7021  findcard  7038  findcard2  7039  findcard2s  7040  fieq0  7131  isotilem  7161  supisolem  7163  inflbti  7179  ordiso2  7190  djuex  7198  updjudhcoinlf  7235  updjudhcoinrg  7236  updjud  7237  ctssdccl  7266  enumctlemm  7269  nnnninf  7281  finomni  7295  pm54.43  7351  acfun  7377  ccfunen  7438  cc2lem  7440  cc3  7442  addclpi  7502  addasspig  7505  mulasspig  7507  addnidpig  7511  nnppipi  7518  ltanqi  7577  ltmnqi  7578  ltexnqq  7583  archnqq  7592  prarloclemarch2  7594  enq0sym  7607  enq0tr  7609  nqnq0pi  7613  nqnq0  7616  mulcanenq0ec  7620  addclnq0  7626  nqpnq0nq  7628  distrnq0  7634  addassnq0lemcl  7636  addassnq0  7637  prubl  7661  prarloclemlt  7668  genpdf  7683  genipv  7684  genpelvl  7687  genpelvu  7688  genpml  7692  genpmu  7693  genprndl  7696  genprndu  7697  genpassl  7699  genpassu  7700  genpassg  7701  addnqprl  7704  addnqpru  7705  addlocpr  7711  nqprm  7717  nqprl  7726  nqpru  7727  mulnqprl  7743  mulnqpru  7744  mullocprlem  7745  mullocpr  7746  addcomprg  7753  mulcomprg  7755  distrlem1prl  7757  distrlem1pru  7758  distrlem4prl  7759  distrlem4pru  7760  ltprordil  7764  1idprl  7765  1idpru  7766  ltpopr  7770  ltsopr  7771  ltaddpr  7772  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemlol  7777  ltexprlemopu  7778  ltexprlemupu  7779  ltexprlemdisj  7781  ltexprlemloc  7782  ltexprlemfl  7784  ltexprlemrl  7785  ltexprlemfu  7786  ltexprlemru  7787  addcanprleml  7789  addcanprlemu  7790  prplnqu  7795  recexprlemloc  7806  recexprlem1ssl  7808  recexprlem1ssu  7809  recexprlemss1l  7810  recexprlemss1u  7811  aptiprleml  7814  aptiprlemu  7815  cauappcvgprlemloc  7827  cauappcvgprlemladdru  7831  cauappcvgprlemladdrl  7832  caucvgprlemloc  7850  caucvgprlemladdrl  7853  caucvgprprlemml  7869  caucvgprprlemloc  7878  00sr  7944  map2psrprg  7980  suplocsrlempr  7982  suplocsrlem  7983  adddir  8125  axsuploc  8207  eqle  8226  le2tri3i  8243  mul4  8266  muladd11  8267  cnegexlem3  8311  addsub12  8347  2addsub  8348  addsubeq4  8349  subadd4  8378  negcon1  8386  negdi2  8392  negsubdi2  8393  neg2sub  8394  renegcl  8395  muladd  8518  subdir  8520  gt0ne0  8562  ltnegcon1  8598  lenegcon1  8601  eqord1  8618  eqord2  8619  recexre  8713  ltmul1  8727  recexap  8788  div12ap  8829  rerecapb  8978  p1le  8984  ltmul2  8991  gt0div  9005  ge0div  9006  zlem1lt  9491  nnaddm1cl  9496  zdceq  9510  gtndiv  9530  prime  9534  msqznn  9535  btwnz  9554  uzss  9731  eluzadd  9739  nn0pzuz  9770  supinfneg  9778  infsupneg  9779  divfnzn  9804  qnegcl  9819  qreccl  9825  elpqb  9833  xaddass  10053  xleadd1a  10057  xlesubadd  10067  elico2  10121  iccss  10125  iccsupr  10150  elfz5  10201  fznn  10273  difelfznle  10319  fzoaddel  10380  elincfzoext  10386  qdceq  10451  qbtwnxr  10464  flqbi2  10498  adddivflid  10499  fldivnn0  10502  divfl0  10503  flqmulnn0  10506  fldivnn0le  10510  fldiv4p1lem1div2  10512  ceiqle  10522  flqdiv  10530  modqmulnn  10551  frecuzrdgtcl  10621  frecuzrdgsuc  10623  frecuzrdgdomlem  10626  frecuzrdgfunlem  10628  frecuzrdgsuctlem  10632  seqm1g  10683  seq3caopr2  10702  seqcaopr2g  10703  iseqf1olemkle  10706  seq3f1olemp  10724  seqf1oglem2  10729  seqf1og  10730  seq3id  10734  seq3z  10737  expap0  10778  mulexp  10787  mulexpzap  10788  expmul  10793  leexp1a  10803  expubnd  10805  zesq  10867  bernneq  10869  bernneq3  10871  modqexp  10875  facdiv  10947  facndiv  10948  faclbnd3  10952  faclbnd6  10953  bccmpl  10963  bcpasc  10975  bccl  10976  seq3coll  11051  fundm2domnop  11055  wrdsymb1  11094  ccatfv0  11124  ccatrn  11130  ccat2s1cl  11152  lswccats1fst  11161  swrdspsleq  11185  pfxtrcfv  11211  pfxsuffeqwrdeq  11216  pfxlswccat  11231  wrdeqs1cat  11238  cats1un  11239  swrdccatin1  11243  pfxccatin12lem4  11244  swrdccatin2  11247  pfxccatin12  11251  swrdccat  11253  shftlem  11313  ovshftex  11316  shftval4  11325  shftf  11327  shftcan2  11332  crim  11355  mulreap  11361  remul2  11370  immul2  11377  cjexp  11390  caucvgre  11478  r19.2uz  11490  sqrtsq2  11540  absnid  11570  absexp  11576  nn0abscl  11582  abslt  11585  lenegsq  11592  cau3lem  11611  minmax  11727  xrmaxadd  11758  clim  11778  climshftlemg  11799  climcn1  11805  climcn1lem  11816  clim2ser  11834  clim2ser2  11835  iserex  11836  isermulc2  11837  climub  11841  climcaucn  11848  serf0  11849  summodclem3  11877  summodclem2a  11878  summodclem2  11879  summodc  11880  fsum3  11884  fsumf1o  11887  fisumss  11889  isumss2  11890  fsumcl2lem  11895  fsumadd  11903  fsumsplit  11904  isummulc2  11923  fsum2d  11932  fsummulc2  11945  telfsumo  11963  fsumparts  11967  hash2iun1dif1  11977  bcxmas  11986  isumshft  11987  isumsplit  11988  expcnvap0  11999  geolim  12008  geolim2  12009  cvgratnnlemmn  12022  cvgratnnlemseq  12023  mertenslemi1  12032  mertenslem2  12033  mertensabs  12034  clim2divap  12037  prodmodclem3  12072  prodmodclem2a  12073  fprodseq  12080  fprodf1o  12085  fprodmul  12088  fprodsplitdc  12093  efcllemp  12155  reefcl  12165  efcj  12170  efaddlem  12171  efexp  12179  reeftlcl  12186  eftlub  12187  efsep  12188  effsumlt  12189  eflegeo  12198  retanclap  12219  demoivre  12270  demoivreALT  12271  eirraplem  12274  dvdsval3  12288  p1modz1  12291  iddvdsexp  12312  alzdvds  12351  addmodlteqALT  12356  nnehalf  12401  nno  12403  ndvdsadd  12428  bitsp1e  12449  bitsp1o  12450  bitsinv1  12459  divgcdnnr  12483  neggcd  12490  gcdabs  12495  bezoutlemmain  12505  bezoutlemaz  12510  bezoutlembz  12511  gcdmultiplez  12528  gcdzeq  12529  dvdssq  12538  nninfctlemfo  12547  algrf  12553  algcvg  12556  algcvga  12559  algfx  12560  eucalgf  12563  eucalgcvga  12566  neglcm  12583  lcmabs  12584  lcmdvds  12587  lcmgcdeq  12591  qredeq  12604  isprm3  12626  coprm  12652  prmrp  12653  isprm6  12655  prmdvdsexpb  12657  rpexp  12661  cncongrprm  12665  sqrt2irraplemnn  12687  phibndlem  12724  phiprmpw  12730  eulerthlemh  12739  eulerthlemth  12740  fermltl  12742  prmdivdiv  12745  modprm1div  12756  m1dvdsndvds  12757  coprimeprodsq  12766  pczpre  12806  pczcl  12807  pcexp  12818  pczdvds  12823  pczndvds  12825  pczndvds2  12827  pcdvdsb  12829  pcneg  12834  pcprmpw  12843  difsqpwdvds  12847  pcmptcl  12851  pcprod  12855  fldivp1  12857  infpnlem2  12869  1arithlem4  12875  ennnfonelemrn  12976  topnidg  13271  pwselbasb  13312  pwsplusgval  13314  pwsmulrval  13315  imasaddfnlemg  13333  imasaddflemg  13335  qusin  13345  mgmlrid  13398  mndass  13443  prdsidlem  13466  mhmco  13509  gsumsubm  13513  gsumwcl  13516  gsumwmhm  13517  grpass  13528  grpinvex  13529  dfgrp2  13546  grplid  13550  grprid  13551  grprcan  13556  grpinvssd  13596  grpinvval2  13602  prdsinvlem  13627  pwsinvg  13631  mhmid  13638  mhmmnd  13639  ghmgrp  13641  mulgnn  13649  mulgnnp1  13653  mulgnegnn  13655  mulgnnsubcl  13657  mulgz  13673  issubg2m  13712  issubg4m  13716  subgintm  13721  nmzbi  13732  eqger  13747  eqgid  13749  eqgen  13750  qusgrp  13755  qusadd  13757  qusinv  13759  qussub  13760  ghminv  13773  ghmsub  13774  ghmrn  13780  resghm2b  13785  ghmf1  13796  conjsubg  13800  conjsubgen  13801  qusghm  13805  cmncom  13825  ablsubadd  13835  ablsubsub23  13848  ghmcmn  13850  gsumfzreidx  13860  mgpress  13880  srg1expzeq1  13944  ringinvnz1ne0  13998  ringinvnzdiv  13999  dvdsrd  14043  dvdsunit  14061  unitinvcl  14072  unitinvinv  14073  unitlinv  14075  unitrinv  14076  rhmunitinv  14127  subrngintm  14161  subrg1  14180  subrguss  14185  subrginv  14186  subrgunit  14188  subrgugrp  14189  subrgintm  14192  resrhm  14197  resrhm2b  14198  lmodass  14252  lmodlcan  14253  lmod0vlid  14267  lmod0vrid  14268  lmod0vid  14269  lmodvs0  14271  lcomf  14276  lmodvnegcl  14277  lmodvnegid  14278  lmodvsubadd  14287  lmodsubid  14296  lss1d  14332  lspval  14339  lspsnel6  14357  lspsnneg  14369  sralmod  14399  dflidl2rng  14430  lidlacl  14433  dflidl2  14437  df2idl2  14458  qusmul2  14478  quscrng  14482  cnfldmulg  14525  znf1o  14600  znidom  14606  psraddcl  14629  psr0lid  14631  tgss3  14737  clsval  14770  clsss3  14789  neiss2  14801  resttop  14829  resttopon2  14837  lmconst  14875  cnima  14879  cnntri  14883  cncnp  14889  cnrest  14894  cndis  14900  lmss  14905  lmff  14908  lmtopcnp  14909  txcnp  14930  upxp  14931  uptx  14933  cnmpt11  14942  hmeoima  14969  hmeoopn  14970  hmeocld  14971  hmeontr  14972  hmeoimaf1o  14973  mettri2  15021  met0  15023  metres2  15040  blpnf  15059  xblss2ps  15063  xblss2  15064  blbas  15092  blres  15093  xmetec  15096  mopnss  15109  xmstri2  15129  mstri2  15130  xmstri  15131  mstri  15132  xmstri3  15133  mstri3  15134  msrtri  15135  mopni3  15143  unimopn  15145  comet  15158  bdxmet  15160  climcncf  15243  dedekindeulemuub  15276  dedekindicclemuub  15285  ivthdichlem  15310  dvfgg  15347  dvidlemap  15350  dvidrelem  15351  dvidsslem  15352  dvfre  15369  dvmptfsum  15384  plyadd  15410  plymul  15411  reeff1olem  15430  reeff1o  15432  sinperlem  15467  abssinper  15505  reexplog  15530  relogexp  15531  cxpexpnn  15555  cxprec  15569  rpcxpmul2  15572  abscxp  15574  wilthlem1  15639  sgmval2  15643  sgmnncl  15647  0sgmppw  15652  perfectlem1  15658  lgsdir  15699  lgsprme0  15706  lgsdinn0  15712  gausslemma2dlem3  15727  gausslemma2dlem5a  15729  2lgslem1a2  15751  2lgslem1a  15752  2lgslem3  15765  2lgs  15768  umgredgprv  15900  umgrislfupgrdom  15914  uspgredgiedg  15961  uspgriedgedg  15962  usgrislfuspgrdom  15973  usgredg2en  15978  usgredgprv  15979  usgrpredgv  15981  usgredg  15983  usgrnloopv  15984  usgredgne  15987  usgredg3  15997  usgredgedg  16010  usgredgdomord  16013  bj-inex  16200  bj-nn0suc  16257  bj-nn0sucALT  16271  trilpolemeq1  16339  trilpolemlt1  16340  trirec0  16343  nconstwlpolemgt0  16363