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  4215  otexg  4372  opelopabt  4406  sonr  4464  sotr  4465  issod  4466  so2nr  4468  so3nr  4469  ordelss  4526  onelon  4531  elrnmpt1s  5034  iota2  5370  funeu  5405  imadif  5464  fnbr  5488  feu  5577  f1ss  5607  f1ssres  5610  f1resf1  5611  dffo2  5622  foco  5629  foun  5661  fun11iun  5663  ffoss  5675  funbrfv  5742  fvco3  5779  fvopab6  5808  funfvbrb  5825  elpreima  5831  ffvelcdm  5844  ffvelcdmda  5846  dffo4  5859  fmptco  5877  fsn2  5885  fncofn  5896  fvconst2g  5932  fex  5950  funfvima  5953  f1elima  5982  f1ocnvfv1  5986  f1ocnvfv2  5987  cocan2  5997  foeqcnvco  5999  isocnv  6020  isores2  6022  isoini  6027  isoselem  6029  f1oiso  6035  f1ofveu  6076  eloprabga  6178  suppssof1  6324  ofco  6325  offveqb  6326  ofc1g  6328  ofc2g  6329  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  fnexALT  6344  f1dmex  6349  ot1stg  6390  ot2ndg  6391  ot3rdgg  6392  eqopi  6410  2ndrn  6421  fo2ndf  6467  suppval1  6483  ressuppss  6498  suppssrst  6505  suppssrgst  6506  smores3  6569  smores2  6570  smoel  6576  smoiso  6578  tfrlem1  6584  tfrlemisucaccv  6601  tfrlemibxssdm  6603  tfrlemiubacc  6606  tfr1onlemsucaccv  6617  tfr1onlembfn  6620  tfr1onlemubacc  6622  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembfn  6633  tfrcllemubacc  6635  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  frecrdg  6684  omv2  6743  nnasuc  6754  nnmsuc  6755  nnacom  6762  nnaass  6763  nnmass  6765  nntri1  6774  nndifsnid  6785  nnmordi  6794  swoer  6840  erth  6858  riinerm  6887  qliftlem  6892  ecovass  6923  ecoviass  6924  elmapssres  6959  fvixp  6991  f1domg  7050  domssr  7070  endomtr  7083  xpsnen2g  7133  enen1  7146  enen2  7147  domen1  7148  domen2  7149  mapen  7152  mapxpen  7154  ssenen  7158  phplem1  7159  fidifsnid  7179  findcard  7198  findcard2  7199  findcard2s  7200  fidcen  7209  relresfin  7270  isfsuppf  7298  fieq0  7316  isotilem  7353  supisolem  7355  inflbti  7371  ordiso2  7382  djuex  7390  updjudhcoinlf  7427  updjudhcoinrg  7428  updjud  7429  ctssdccl  7458  enumctlemm  7461  nnnninf  7473  finomni  7487  pm54.43  7543  acfun  7570  ccfunen  7637  cc2lem  7639  cc3  7641  addclpi  7701  addasspig  7704  mulasspig  7706  addnidpig  7710  nnppipi  7717  ltanqi  7776  ltmnqi  7777  ltexnqq  7782  archnqq  7791  prarloclemarch2  7793  enq0sym  7806  enq0tr  7808  nqnq0pi  7812  nqnq0  7815  mulcanenq0ec  7819  addclnq0  7825  nqpnq0nq  7827  distrnq0  7833  addassnq0lemcl  7835  addassnq0  7836  prubl  7860  prarloclemlt  7867  genpdf  7882  genipv  7883  genpelvl  7886  genpelvu  7887  genpml  7891  genpmu  7892  genprndl  7895  genprndu  7896  genpassl  7898  genpassu  7899  genpassg  7900  addnqprl  7903  addnqpru  7904  addlocpr  7910  nqprm  7916  nqprl  7925  nqpru  7926  mulnqprl  7942  mulnqpru  7943  mullocprlem  7944  mullocpr  7945  addcomprg  7952  mulcomprg  7954  distrlem1prl  7956  distrlem1pru  7957  distrlem4prl  7958  distrlem4pru  7959  ltprordil  7963  1idprl  7964  1idpru  7965  ltpopr  7969  ltsopr  7970  ltaddpr  7971  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemdisj  7980  ltexprlemloc  7981  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  prplnqu  7994  recexprlemloc  8005  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010  aptiprleml  8013  aptiprlemu  8014  cauappcvgprlemloc  8026  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemloc  8049  caucvgprlemladdrl  8052  caucvgprprlemml  8068  caucvgprprlemloc  8077  00sr  8143  map2psrprg  8179  suplocsrlempr  8181  suplocsrlem  8182  adddir  8324  axsuploc  8405  eqle  8424  le2tri3i  8442  mul4  8466  muladd11  8467  cnegexlem3  8511  addsub12  8547  2addsub  8548  addsubeq4  8549  subadd4  8578  negcon1  8586  negdi2  8592  negsubdi2  8593  neg2sub  8594  renegcl  8595  muladd  8719  subdir  8721  gt0ne0  8763  ltnegcon1  8799  lenegcon1  8802  eqord1  8819  eqord2  8820  recexre  8915  ltmul1  8929  recexap  8990  div12ap  9033  rerecapb  9182  p1le  9188  ltmul2  9195  gt0div  9209  ge0div  9210  zlem1lt  9711  nnaddm1cl  9716  zdceq  9730  gtndiv  9752  prime  9756  msqznn  9757  btwnz  9776  uzss  9959  eluzadd  9967  nn0pzuz  10003  supinfneg  10011  infsupneg  10012  divfnzn  10037  qnegcl  10052  qreccl  10058  elpqb  10067  xaddass  10288  xleadd1a  10292  xlesubadd  10302  elico2  10356  iccss  10360  iccsupr  10385  elfz5  10437  fznn  10513  difelfznle  10559  fzoaddel  10622  elincfzoext  10628  qdceq  10696  qbtwnxr  10709  flqbi2  10747  adddivflid  10748  fldivnn0  10751  divfl0  10752  flqmulnn0  10755  fldivnn0le  10759  fldiv4p1lem1div2  10761  ceiqle  10771  flqdiv  10779  modqmulnn  10800  frecuzrdgtcl  10870  frecuzrdgsuc  10872  frecuzrdgdomlem  10875  frecuzrdgfunlem  10877  frecuzrdgsuctlem  10881  seqm1g  10932  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemkle  10955  seq3f1olemp  10973  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3z  10986  expap0  11027  mulexp  11036  mulexpzap  11037  expmul  11042  leexp1a  11052  expubnd  11054  zesq  11117  bernneq  11119  bernneq3  11121  modqexp  11125  facdiv  11198  facndiv  11199  faclbnd3  11203  faclbnd6  11204  bccmpl  11214  bcpasc  11226  bccl  11227  hashfibclem  11304  hashfibc  11305  seq3coll  11316  fundm2domnop  11323  wrdsymb1  11363  ccatfv0  11393  ccatrn  11399  ccat2s1cl  11423  lswccats1fst  11434  swrdspsleq  11461  pfxtrcfv  11487  pfxsuffeqwrdeq  11492  pfxlswccat  11507  wrdeqs1cat  11514  cats1un  11515  swrdccatin1  11519  pfxccatin12lem4  11520  swrdccatin2  11523  pfxccatin12  11527  swrdccat  11529  shftlem  11603  ovshftex  11606  shftval4  11615  shftf  11617  shftcan2  11622  crim  11645  mulreap  11651  remul2  11660  immul2  11667  cjexp  11680  caucvgre  11769  r19.2uz  11781  sqrtsq2  11831  absnid  11861  absexp  11868  nn0abscl  11874  abslt  11877  lenegsq  11884  cau3lem  11903  minmax  12020  xrmaxadd  12052  clim  12072  climshftlemg  12093  climcn1  12099  climcn1lem  12110  clim2ser  12128  clim2ser2  12129  iserex  12130  isermulc2  12131  climub  12135  climcaucn  12142  serf0  12143  summodclem3  12172  summodclem2a  12173  summodclem2  12174  summodc  12175  fsum3  12179  fsumf1o  12182  fisumss  12184  isumss2  12185  fsumcl2lem  12190  fsumadd  12198  fsumsplit  12199  isummulc2  12218  fsum2d  12227  fsummulc2  12240  telfsumo  12258  fsumparts  12262  hash2iun1dif1  12272  bcxmas  12281  isumshft  12282  isumsplit  12283  expcnvap0  12294  geolim  12303  geolim2  12304  cvgratnnlemmn  12317  cvgratnnlemseq  12318  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  clim2divap  12332  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodf1o  12380  fprodmul  12383  fprodsplitdc  12388  efcllemp  12450  reefcl  12460  efcj  12465  efaddlem  12466  efexp  12474  reeftlcl  12481  eftlub  12482  efsep  12483  effsumlt  12484  eflegeo  12493  retanclap  12514  demoivre  12565  demoivreALT  12566  eirraplem  12569  dvdsval3  12583  p1modz1  12586  iddvdsexp  12607  alzdvds  12646  addmodlteqALT  12651  nnehalf  12696  nno  12698  ndvdsadd  12723  bitsp1e  12744  bitsp1o  12745  bitsinv1  12754  divgcdnnr  12778  neggcd  12785  gcdabs  12790  bezoutlemmain  12800  bezoutlemaz  12805  bezoutlembz  12806  gcdmultiplez  12823  gcdzeq  12824  dvdssq  12833  nninfctlemfo  12842  algrf  12848  algcvg  12851  algcvga  12854  algfx  12855  eucalgf  12858  eucalgcvga  12861  neglcm  12878  lcmabs  12879  lcmdvds  12882  lcmgcdeq  12886  qredeq  12899  isprm3  12921  coprm  12948  prmrp  12949  isprm6  12951  prmdvdsexpb  12953  rpexp  12957  cncongrprm  12961  sqrt2irraplemnn  12984  phibndlem  13023  phiprmpw  13029  eulerthlemh  13038  eulerthlemth  13039  fermltl  13041  prmdivdiv  13044  modprm1div  13055  m1dvdsndvds  13056  coprimeprodsq  13065  pczpre  13105  pczcl  13106  pcexp  13117  pczdvds  13122  pczndvds  13124  pczndvds2  13126  pcdvdsb  13128  pcneg  13133  pcprmpw  13142  difsqpwdvds  13146  pcmptcl  13150  pcprod  13154  fldivp1  13156  infpnlem2  13168  1arithlem4  13174  prmlem0  13249  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrcn0  13331  ennnfonelemrn  13368  topnidg  13665  imasaddfnlemg  13694  imasaddflemg  13696  qusin  13706  mgmlrid  13758  mndass  13796  mhmco  13856  gzsumwcl  13861  gzsumwmhm  13862  grpass  13873  grpinvex  13874  dfgrp2  13891  grplid  13895  grprid  13896  grprcan  13901  grpinvssd  13941  grpinvval2  13947  mhmid  13977  mhmmnd  13978  ghmgrp  13980  mulgnn  13988  mulgnnp1  13992  mulgnegnn  13994  mulgnnsubcl  13996  mulgz  14012  issubg2m  14051  issubg4m  14055  subgintm  14060  nmzbi  14071  eqger  14086  eqgid  14088  eqgen  14089  qusgrp  14094  qusadd  14096  qusinv  14098  qussub  14099  ghminv  14112  ghmsub  14113  ghmrn  14119  resghm2b  14124  ghmf1  14135  conjsubg  14139  conjsubgen  14140  qusghm  14144  cntzi  14162  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  cmncom  14195  ablsubadd  14206  ablsubsub23  14219  ghmcmn  14221  gzsumreidx  14231  gsummptfidmsplit  14254  gsumsubmfi  14268  prdsidlem  14300  prdsinvlem  14303  pwselbasb  14313  pwsplusgval  14315  pwsmulrval  14316  pwsinvg  14322  mgpress  14337  srg1expzeq1  14406  ringinvnz1ne0  14461  ringinvnzdiv  14462  dvdsrd  14510  dvdsunit  14528  unitinvcl  14539  unitinvinv  14540  unitlinv  14542  unitrinv  14543  rhmunitinv  14594  subrngintm  14629  subrg1  14648  subrguss  14653  subrginv  14654  subrgunit  14656  subrgugrp  14657  subrgintm  14660  resrhm  14665  resrhm2b  14666  lmodass  14748  lmodlcan  14749  lmod0vlid  14764  lmod0vrid  14765  lmod0vid  14766  lmodvs0  14768  lcomf  14773  lmodvnegcl  14774  lmodvnegid  14775  lmodvsubadd  14784  lmodsubid  14793  lss1d  14829  lspval  14836  ellspsn6  14854  lspsnneg  14866  sralmod  14896  dflidl2rng  14927  lidlacl  14930  dflidl2  14934  df2idl2  14955  qusmul2  14975  quscrng  14979  cnfldmulg  15022  znf1o  15095  znidom  15101  aspval  15124  asclghm  15134  issubassa2  15144  gsumbagdiagfi  15195  psrass1filem  15196  psraddcl  15203  psrmulvalfi  15207  psr0lid  15212  psrlidmfi  15219  mvrclfi  15238  mplsubgfilemcl  15246  tgss3  15337  clsval  15370  clsss3  15389  neiss2  15401  resttop  15429  resttopon2  15437  lmconst  15475  cnima  15479  cnntri  15483  cncnp  15489  cnrest  15494  cndis  15500  lmss  15505  lmff  15508  lmtopcnp  15509  txcnp  15530  upxp  15531  uptx  15533  cnmpt11  15542  hmeoima  15569  hmeoopn  15570  hmeocld  15571  hmeontr  15572  hmeoimaf1o  15573  mettri2  15621  met0  15623  metres2  15640  blpnf  15659  xblss2ps  15663  xblss2  15664  blbas  15692  blres  15693  xmetec  15696  mopnss  15709  xmstri2  15729  mstri2  15730  xmstri  15731  mstri  15732  xmstri3  15733  mstri3  15734  msrtri  15735  mopni3  15743  unimopn  15745  comet  15758  bdxmet  15760  climcncf  15843  dedekindeulemuub  15876  dedekindicclemuub  15885  ivthdichlem  15910  dvfgg  15947  dvidlemap  15950  dvidrelem  15951  dvidsslem  15952  dvfre  15969  dvmptfsum  15984  plyadd  16010  plymul  16011  reeff1olem  16030  reeff1o  16032  sinperlem  16068  abssinper  16106  reexplog  16134  relogexp  16135  cxpexpnn  16162  cxprec  16176  rpcxpmul2  16179  abscxp  16183  wilthlem1  16265  ppival2g  16283  sgmval2  16286  sgmnncl  16290  0sgmppw  16320  chtublem  16328  perfectlem1  16332  bposlem3  16346  bposlem5  16348  bposlem6  16349  lgsdir  16392  lgsprme0  16399  lgsdinn0  16405  gausslemma2dlem3  16420  gausslemma2dlem5a  16422  2lgslem1a2  16444  2lgslem1a  16445  2lgslem3  16458  2lgs  16461  umgredgprv  16594  umgrislfupgrdom  16610  uspgredgiedg  16657  uspgriedgedg  16658  usgrislfuspgrdom  16669  usgredg2en  16674  usgredgprv  16675  usgrpredgv  16677  usgredg  16679  usgrnloopv  16680  usgredgne  16683  usgredg3  16693  usgredgedg  16706  usgredgdomord  16709  usgr1vr  16727  subgruhgrfun  16747  subupgr  16752  subumgr  16753  subusgr  16754  umgrwlknloop  16847  wlkres  16858  clwwlkccatlem  16879  clwwlkccat  16880  depindlem1  16985  depindlem2  16986  depindlem3  16987  bj-inex  17171  bj-nn0suc  17228  bj-nn0sucALT  17242  trilpolemeq1  17329  trilpolemlt1  17330  trirec0  17333  nconstwlpolemgt0  17354