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  941  3adantl1  1156  3adantl2  1157  3adantl3  1158  syl3anl1  1298  syl3anl3  1300  syl3anl  1301  stoic3  1451  eupick  2134  csbiebt  3137  csbnestgf  3150  reuss2  3457  mpteq12  4138  otexg  4287  opelopabt  4321  sonr  4377  sotr  4378  issod  4379  so2nr  4381  so3nr  4382  ordelss  4439  onelon  4444  elrnmpt1s  4942  iota2  5275  funeu  5310  imadif  5368  fnbr  5392  feu  5475  f1ss  5504  f1ssres  5507  f1resf1  5508  dffo2  5519  foco  5526  foun  5558  fun11iun  5560  ffoss  5571  funbrfv  5635  fvco3  5668  fvopab6  5694  funfvbrb  5711  elpreima  5717  ffvelcdm  5731  ffvelcdmda  5733  dffo4  5746  fmptco  5764  fsn2  5772  fvconst2g  5816  fex  5831  funfvima  5834  f1elima  5860  f1ocnvfv1  5864  f1ocnvfv2  5865  cocan2  5875  foeqcnvco  5877  isocnv  5898  isores2  5900  isoini  5905  isoselem  5907  f1oiso  5913  f1ofveu  5950  eloprabga  6050  suppssof1  6194  ofco  6195  offveqb  6196  ofc1g  6198  ofc2g  6199  caofid0l  6203  caofid0r  6204  caofid1  6205  caofid2  6206  fnexALT  6214  f1dmex  6219  ot1stg  6256  ot2ndg  6257  ot3rdgg  6258  eqopi  6276  2ndrn  6287  fo2ndf  6331  smores3  6397  smores2  6398  smoel  6404  smoiso  6406  tfrlem1  6412  tfrlemisucaccv  6429  tfrlemibxssdm  6431  tfrlemiubacc  6434  tfr1onlemsucaccv  6445  tfr1onlembfn  6448  tfr1onlemubacc  6450  tfr1onlemaccex  6452  tfr1onlemres  6453  tfrcllemsucaccv  6458  tfrcllembfn  6461  tfrcllemubacc  6463  tfrcllemaccex  6465  tfrcllemres  6466  tfrcl  6468  frecrdg  6512  omv2  6569  nnasuc  6580  nnmsuc  6581  nnacom  6588  nnaass  6589  nnmass  6591  nntri1  6600  nndifsnid  6611  nnmordi  6620  swoer  6666  erth  6684  riinerm  6713  qliftlem  6718  ecovass  6749  ecoviass  6750  elmapssres  6778  fvixp  6808  f1domg  6867  domssr  6887  endomtr  6900  xpsnen2g  6944  enen1  6957  enen2  6958  domen1  6959  domen2  6960  mapen  6963  mapxpen  6965  ssenen  6968  phplem1  6969  fidifsnid  6989  findcard  7006  findcard2  7007  findcard2s  7008  fieq0  7099  isotilem  7129  supisolem  7131  inflbti  7147  ordiso2  7158  djuex  7166  updjudhcoinlf  7203  updjudhcoinrg  7204  updjud  7205  ctssdccl  7234  enumctlemm  7237  nnnninf  7249  finomni  7263  pm54.43  7319  acfun  7345  ccfunen  7406  cc2lem  7408  cc3  7410  addclpi  7470  addasspig  7473  mulasspig  7475  addnidpig  7479  nnppipi  7486  ltanqi  7545  ltmnqi  7546  ltexnqq  7551  archnqq  7560  prarloclemarch2  7562  enq0sym  7575  enq0tr  7577  nqnq0pi  7581  nqnq0  7584  mulcanenq0ec  7588  addclnq0  7594  nqpnq0nq  7596  distrnq0  7602  addassnq0lemcl  7604  addassnq0  7605  prubl  7629  prarloclemlt  7636  genpdf  7651  genipv  7652  genpelvl  7655  genpelvu  7656  genpml  7660  genpmu  7661  genprndl  7664  genprndu  7665  genpassl  7667  genpassu  7668  genpassg  7669  addnqprl  7672  addnqpru  7673  addlocpr  7679  nqprm  7685  nqprl  7694  nqpru  7695  mulnqprl  7711  mulnqpru  7712  mullocprlem  7713  mullocpr  7714  addcomprg  7721  mulcomprg  7723  distrlem1prl  7725  distrlem1pru  7726  distrlem4prl  7727  distrlem4pru  7728  ltprordil  7732  1idprl  7733  1idpru  7734  ltpopr  7738  ltsopr  7739  ltaddpr  7740  ltexprlemm  7743  ltexprlemopl  7744  ltexprlemlol  7745  ltexprlemopu  7746  ltexprlemupu  7747  ltexprlemdisj  7749  ltexprlemloc  7750  ltexprlemfl  7752  ltexprlemrl  7753  ltexprlemfu  7754  ltexprlemru  7755  addcanprleml  7757  addcanprlemu  7758  prplnqu  7763  recexprlemloc  7774  recexprlem1ssl  7776  recexprlem1ssu  7777  recexprlemss1l  7778  recexprlemss1u  7779  aptiprleml  7782  aptiprlemu  7783  cauappcvgprlemloc  7795  cauappcvgprlemladdru  7799  cauappcvgprlemladdrl  7800  caucvgprlemloc  7818  caucvgprlemladdrl  7821  caucvgprprlemml  7837  caucvgprprlemloc  7846  00sr  7912  map2psrprg  7948  suplocsrlempr  7950  suplocsrlem  7951  adddir  8093  axsuploc  8175  eqle  8194  le2tri3i  8211  mul4  8234  muladd11  8235  cnegexlem3  8279  addsub12  8315  2addsub  8316  addsubeq4  8317  subadd4  8346  negcon1  8354  negdi2  8360  negsubdi2  8361  neg2sub  8362  renegcl  8363  muladd  8486  subdir  8488  gt0ne0  8530  ltnegcon1  8566  lenegcon1  8569  eqord1  8586  eqord2  8587  recexre  8681  ltmul1  8695  recexap  8756  div12ap  8797  rerecapb  8946  p1le  8952  ltmul2  8959  gt0div  8973  ge0div  8974  zlem1lt  9459  nnaddm1cl  9464  zdceq  9478  gtndiv  9498  prime  9502  msqznn  9503  btwnz  9522  uzss  9699  eluzadd  9707  nn0pzuz  9738  supinfneg  9746  infsupneg  9747  divfnzn  9772  qnegcl  9787  qreccl  9793  elpqb  9801  xaddass  10021  xleadd1a  10025  xlesubadd  10035  elico2  10089  iccss  10093  iccsupr  10118  elfz5  10169  fznn  10241  difelfznle  10287  fzoaddel  10348  elincfzoext  10354  qdceq  10419  qbtwnxr  10432  flqbi2  10466  adddivflid  10467  fldivnn0  10470  divfl0  10471  flqmulnn0  10474  fldivnn0le  10478  fldiv4p1lem1div2  10480  ceiqle  10490  flqdiv  10498  modqmulnn  10519  frecuzrdgtcl  10589  frecuzrdgsuc  10591  frecuzrdgdomlem  10594  frecuzrdgfunlem  10596  frecuzrdgsuctlem  10600  seqm1g  10651  seq3caopr2  10670  seqcaopr2g  10671  iseqf1olemkle  10674  seq3f1olemp  10692  seqf1oglem2  10697  seqf1og  10698  seq3id  10702  seq3z  10705  expap0  10746  mulexp  10755  mulexpzap  10756  expmul  10761  leexp1a  10771  expubnd  10773  zesq  10835  bernneq  10837  bernneq3  10839  modqexp  10843  facdiv  10915  facndiv  10916  faclbnd3  10920  faclbnd6  10921  bccmpl  10931  bcpasc  10943  bccl  10944  seq3coll  11019  fundm2domnop  11023  wrdsymb1  11062  ccatfv0  11092  ccatrn  11098  ccat2s1cl  11120  lswccats1fst  11129  swrdspsleq  11153  pfxtrcfv  11179  pfxsuffeqwrdeq  11184  pfxlswccat  11199  wrdeqs1cat  11206  cats1un  11207  shftlem  11212  ovshftex  11215  shftval4  11224  shftf  11226  shftcan2  11231  crim  11254  mulreap  11260  remul2  11269  immul2  11276  cjexp  11289  caucvgre  11377  r19.2uz  11389  sqrtsq2  11439  absnid  11469  absexp  11475  nn0abscl  11481  abslt  11484  lenegsq  11491  cau3lem  11510  minmax  11626  xrmaxadd  11657  clim  11677  climshftlemg  11698  climcn1  11704  climcn1lem  11715  clim2ser  11733  clim2ser2  11734  iserex  11735  isermulc2  11736  climub  11740  climcaucn  11747  serf0  11748  summodclem3  11776  summodclem2a  11777  summodclem2  11778  summodc  11779  fsum3  11783  fsumf1o  11786  fisumss  11788  isumss2  11789  fsumcl2lem  11794  fsumadd  11802  fsumsplit  11803  isummulc2  11822  fsum2d  11831  fsummulc2  11844  telfsumo  11862  fsumparts  11866  hash2iun1dif1  11876  bcxmas  11885  isumshft  11886  isumsplit  11887  expcnvap0  11898  geolim  11907  geolim2  11908  cvgratnnlemmn  11921  cvgratnnlemseq  11922  mertenslemi1  11931  mertenslem2  11932  mertensabs  11933  clim2divap  11936  prodmodclem3  11971  prodmodclem2a  11972  fprodseq  11979  fprodf1o  11984  fprodmul  11987  fprodsplitdc  11992  efcllemp  12054  reefcl  12064  efcj  12069  efaddlem  12070  efexp  12078  reeftlcl  12085  eftlub  12086  efsep  12087  effsumlt  12088  eflegeo  12097  retanclap  12118  demoivre  12169  demoivreALT  12170  eirraplem  12173  dvdsval3  12187  p1modz1  12190  iddvdsexp  12211  alzdvds  12250  addmodlteqALT  12255  nnehalf  12300  nno  12302  ndvdsadd  12327  bitsp1e  12348  bitsp1o  12349  bitsinv1  12358  divgcdnnr  12382  neggcd  12389  gcdabs  12394  bezoutlemmain  12404  bezoutlemaz  12409  bezoutlembz  12410  gcdmultiplez  12427  gcdzeq  12428  dvdssq  12437  nninfctlemfo  12446  algrf  12452  algcvg  12455  algcvga  12458  algfx  12459  eucalgf  12462  eucalgcvga  12465  neglcm  12482  lcmabs  12483  lcmdvds  12486  lcmgcdeq  12490  qredeq  12503  isprm3  12525  coprm  12551  prmrp  12552  isprm6  12554  prmdvdsexpb  12556  rpexp  12560  cncongrprm  12564  sqrt2irraplemnn  12586  phibndlem  12623  phiprmpw  12629  eulerthlemh  12638  eulerthlemth  12639  fermltl  12641  prmdivdiv  12644  modprm1div  12655  m1dvdsndvds  12656  coprimeprodsq  12665  pczpre  12705  pczcl  12706  pcexp  12717  pczdvds  12722  pczndvds  12724  pczndvds2  12726  pcdvdsb  12728  pcneg  12733  pcprmpw  12742  difsqpwdvds  12746  pcmptcl  12750  pcprod  12754  fldivp1  12756  infpnlem2  12768  1arithlem4  12774  ennnfonelemrn  12875  topnidg  13169  pwselbasb  13210  pwsplusgval  13212  pwsmulrval  13213  imasaddfnlemg  13231  imasaddflemg  13233  qusin  13243  mgmlrid  13296  mndass  13341  prdsidlem  13364  mhmco  13407  gsumsubm  13411  gsumwcl  13414  gsumwmhm  13415  grpass  13426  grpinvex  13427  dfgrp2  13444  grplid  13448  grprid  13449  grprcan  13454  grpinvssd  13494  grpinvval2  13500  prdsinvlem  13525  pwsinvg  13529  mhmid  13536  mhmmnd  13537  ghmgrp  13539  mulgnn  13547  mulgnnp1  13551  mulgnegnn  13553  mulgnnsubcl  13555  mulgz  13571  issubg2m  13610  issubg4m  13614  subgintm  13619  nmzbi  13630  eqger  13645  eqgid  13647  eqgen  13648  qusgrp  13653  qusadd  13655  qusinv  13657  qussub  13658  ghminv  13671  ghmsub  13672  ghmrn  13678  resghm2b  13683  ghmf1  13694  conjsubg  13698  conjsubgen  13699  qusghm  13703  cmncom  13723  ablsubadd  13733  ablsubsub23  13746  ghmcmn  13748  gsumfzreidx  13758  mgpress  13778  srg1expzeq1  13842  ringinvnz1ne0  13896  ringinvnzdiv  13897  dvdsrd  13941  dvdsunit  13959  unitinvcl  13970  unitinvinv  13971  unitlinv  13973  unitrinv  13974  rhmunitinv  14025  subrngintm  14059  subrg1  14078  subrguss  14083  subrginv  14084  subrgunit  14086  subrgugrp  14087  subrgintm  14090  resrhm  14095  resrhm2b  14096  lmodass  14150  lmodlcan  14151  lmod0vlid  14165  lmod0vrid  14166  lmod0vid  14167  lmodvs0  14169  lcomf  14174  lmodvnegcl  14175  lmodvnegid  14176  lmodvsubadd  14185  lmodsubid  14194  lss1d  14230  lspval  14237  lspsnel6  14255  lspsnneg  14267  sralmod  14297  dflidl2rng  14328  lidlacl  14331  dflidl2  14335  df2idl2  14356  qusmul2  14376  quscrng  14380  cnfldmulg  14423  znf1o  14498  znidom  14504  psraddcl  14527  psr0lid  14529  tgss3  14635  clsval  14668  clsss3  14687  neiss2  14699  resttop  14727  resttopon2  14735  lmconst  14773  cnima  14777  cnntri  14781  cncnp  14787  cnrest  14792  cndis  14798  lmss  14803  lmff  14806  lmtopcnp  14807  txcnp  14828  upxp  14829  uptx  14831  cnmpt11  14840  hmeoima  14867  hmeoopn  14868  hmeocld  14869  hmeontr  14870  hmeoimaf1o  14871  mettri2  14919  met0  14921  metres2  14938  blpnf  14957  xblss2ps  14961  xblss2  14962  blbas  14990  blres  14991  xmetec  14994  mopnss  15007  xmstri2  15027  mstri2  15028  xmstri  15029  mstri  15030  xmstri3  15031  mstri3  15032  msrtri  15033  mopni3  15041  unimopn  15043  comet  15056  bdxmet  15058  climcncf  15141  dedekindeulemuub  15174  dedekindicclemuub  15183  ivthdichlem  15208  dvfgg  15245  dvidlemap  15248  dvidrelem  15249  dvidsslem  15250  dvfre  15267  dvmptfsum  15282  plyadd  15308  plymul  15309  reeff1olem  15328  reeff1o  15330  sinperlem  15365  abssinper  15403  reexplog  15428  relogexp  15429  cxpexpnn  15453  cxprec  15467  rpcxpmul2  15470  abscxp  15472  wilthlem1  15537  sgmval2  15541  sgmnncl  15545  0sgmppw  15550  perfectlem1  15556  lgsdir  15597  lgsprme0  15604  lgsdinn0  15610  gausslemma2dlem3  15625  gausslemma2dlem5a  15627  2lgslem1a2  15649  2lgslem1a  15650  2lgslem3  15663  2lgs  15666  umgrislfupgrdom  15807  bj-inex  16012  bj-nn0suc  16069  bj-nn0sucALT  16083  trilpolemeq1  16151  trilpolemlt1  16152  trirec0  16155  nconstwlpolemgt0  16175