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  6568  smores2  6569  smoel  6575  smoiso  6577  tfrlem1  6583  tfrlemisucaccv  6600  tfrlemibxssdm  6602  tfrlemiubacc  6605  tfr1onlemsucaccv  6616  tfr1onlembfn  6619  tfr1onlemubacc  6621  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembfn  6632  tfrcllemubacc  6634  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  frecrdg  6683  omv2  6742  nnasuc  6753  nnmsuc  6754  nnacom  6761  nnaass  6762  nnmass  6764  nntri1  6773  nndifsnid  6784  nnmordi  6793  swoer  6839  erth  6857  riinerm  6886  qliftlem  6891  ecovass  6922  ecoviass  6923  elmapssres  6958  fvixp  6990  f1domg  7049  domssr  7069  endomtr  7082  xpsnen2g  7132  enen1  7145  enen2  7146  domen1  7147  domen2  7148  mapen  7151  mapxpen  7153  ssenen  7157  phplem1  7158  fidifsnid  7178  findcard  7197  findcard2  7198  findcard2s  7199  fidcen  7208  relresfin  7269  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  9713  nnaddm1cl  9718  zdceq  9732  gtndiv  9753  prime  9757  msqznn  9758  btwnz  9777  uzss  9960  eluzadd  9968  nn0pzuz  10004  supinfneg  10012  infsupneg  10013  divfnzn  10038  qnegcl  10053  qreccl  10059  elpqb  10068  xaddass  10289  xleadd1a  10293  xlesubadd  10303  elico2  10357  iccss  10361  iccsupr  10386  elfz5  10438  fznn  10514  difelfznle  10560  fzoaddel  10623  elincfzoext  10629  qdceq  10697  qbtwnxr  10710  flqbi2  10748  adddivflid  10749  fldivnn0  10752  divfl0  10753  flqmulnn0  10756  fldivnn0le  10760  fldiv4p1lem1div2  10762  ceiqle  10772  flqdiv  10780  modqmulnn  10801  frecuzrdgtcl  10871  frecuzrdgsuc  10873  frecuzrdgdomlem  10876  frecuzrdgfunlem  10878  frecuzrdgsuctlem  10882  seqm1g  10933  seq3caopr2  10952  seqcaopr2g  10953  iseqf1olemkle  10956  seq3f1olemp  10974  seqf1oglem2  10979  seqf1og  10980  seq3id  10984  seq3z  10987  expap0  11028  mulexp  11037  mulexpzap  11038  expmul  11043  leexp1a  11053  expubnd  11055  zesq  11118  bernneq  11120  bernneq3  11122  modqexp  11126  facdiv  11199  facndiv  11200  faclbnd3  11204  faclbnd6  11205  bccmpl  11215  bcpasc  11227  bccl  11228  hashfibclem  11305  hashfibc  11306  seq3coll  11317  fundm2domnop  11324  wrdsymb1  11364  ccatfv0  11394  ccatrn  11400  ccat2s1cl  11424  lswccats1fst  11435  swrdspsleq  11462  pfxtrcfv  11488  pfxsuffeqwrdeq  11493  pfxlswccat  11508  wrdeqs1cat  11515  cats1un  11516  swrdccatin1  11520  pfxccatin12lem4  11521  swrdccatin2  11524  pfxccatin12  11528  swrdccat  11530  shftlem  11604  ovshftex  11607  shftval4  11616  shftf  11618  shftcan2  11623  crim  11646  mulreap  11652  remul2  11661  immul2  11668  cjexp  11681  caucvgre  11770  r19.2uz  11782  sqrtsq2  11832  absnid  11862  absexp  11869  nn0abscl  11875  abslt  11878  lenegsq  11885  cau3lem  11904  minmax  12021  xrmaxadd  12053  clim  12073  climshftlemg  12094  climcn1  12100  climcn1lem  12111  clim2ser  12129  clim2ser2  12130  iserex  12131  isermulc2  12132  climub  12136  climcaucn  12143  serf0  12144  summodclem3  12173  summodclem2a  12174  summodclem2  12175  summodc  12176  fsum3  12180  fsumf1o  12183  fisumss  12185  isumss2  12186  fsumcl2lem  12191  fsumadd  12199  fsumsplit  12200  isummulc2  12219  fsum2d  12228  fsummulc2  12241  telfsumo  12259  fsumparts  12263  hash2iun1dif1  12273  bcxmas  12282  isumshft  12283  isumsplit  12284  expcnvap0  12295  geolim  12304  geolim2  12305  cvgratnnlemmn  12318  cvgratnnlemseq  12319  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  clim2divap  12333  prodmodclem3  12368  prodmodclem2a  12369  fprodseq  12376  fprodf1o  12381  fprodmul  12384  fprodsplitdc  12389  efcllemp  12451  reefcl  12461  efcj  12466  efaddlem  12467  efexp  12475  reeftlcl  12482  eftlub  12483  efsep  12484  effsumlt  12485  eflegeo  12494  retanclap  12515  demoivre  12566  demoivreALT  12567  eirraplem  12570  dvdsval3  12584  p1modz1  12587  iddvdsexp  12608  alzdvds  12647  addmodlteqALT  12652  nnehalf  12697  nno  12699  ndvdsadd  12724  bitsp1e  12745  bitsp1o  12746  bitsinv1  12755  divgcdnnr  12779  neggcd  12786  gcdabs  12791  bezoutlemmain  12801  bezoutlemaz  12806  bezoutlembz  12807  gcdmultiplez  12824  gcdzeq  12825  dvdssq  12834  nninfctlemfo  12843  algrf  12849  algcvg  12852  algcvga  12855  algfx  12856  eucalgf  12859  eucalgcvga  12862  neglcm  12879  lcmabs  12880  lcmdvds  12883  lcmgcdeq  12887  qredeq  12900  isprm3  12922  coprm  12949  prmrp  12950  isprm6  12952  prmdvdsexpb  12954  rpexp  12958  cncongrprm  12962  sqrt2irraplemnn  12985  phibndlem  13024  phiprmpw  13030  eulerthlemh  13039  eulerthlemth  13040  fermltl  13042  prmdivdiv  13045  modprm1div  13056  m1dvdsndvds  13057  coprimeprodsq  13066  pczpre  13106  pczcl  13107  pcexp  13118  pczdvds  13123  pczndvds  13125  pczndvds2  13127  pcdvdsb  13129  pcneg  13134  pcprmpw  13143  difsqpwdvds  13147  pcmptcl  13151  pcprod  13155  fldivp1  13157  infpnlem2  13169  1arithlem4  13175  prmlem0  13250  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemfrcn0  13332  ennnfonelemrn  13369  topnidg  13666  imasaddfnlemg  13695  imasaddflemg  13697  qusin  13707  mgmlrid  13759  mndass  13797  mhmco  13857  gzsumwcl  13862  gzsumwmhm  13863  grpass  13874  grpinvex  13875  dfgrp2  13892  grplid  13896  grprid  13897  grprcan  13902  grpinvssd  13942  grpinvval2  13948  mhmid  13978  mhmmnd  13979  ghmgrp  13981  mulgnn  13989  mulgnnp1  13993  mulgnegnn  13995  mulgnnsubcl  13997  mulgz  14013  issubg2m  14052  issubg4m  14056  subgintm  14061  nmzbi  14072  eqger  14087  eqgid  14089  eqgen  14090  qusgrp  14095  qusadd  14097  qusinv  14099  qussub  14100  ghminv  14113  ghmsub  14114  ghmrn  14120  resghm2b  14125  ghmf1  14136  conjsubg  14140  conjsubgen  14141  qusghm  14145  cntzi  14163  cntzsgrpcl  14168  cntzsubm  14171  cntzsubg  14172  cmncom  14196  ablsubadd  14207  ablsubsub23  14220  ghmcmn  14222  gzsumreidx  14232  gsummptfidmsplit  14255  gsumsubmfi  14269  prdsidlem  14301  prdsinvlem  14304  pwselbasb  14314  pwsplusgval  14316  pwsmulrval  14317  pwsinvg  14323  mgpress  14338  srg1expzeq1  14407  ringinvnz1ne0  14462  ringinvnzdiv  14463  dvdsrd  14511  dvdsunit  14529  unitinvcl  14540  unitinvinv  14541  unitlinv  14543  unitrinv  14544  rhmunitinv  14595  subrngintm  14630  subrg1  14649  subrguss  14654  subrginv  14655  subrgunit  14657  subrgugrp  14658  subrgintm  14661  resrhm  14666  resrhm2b  14667  lmodass  14749  lmodlcan  14750  lmod0vlid  14765  lmod0vrid  14766  lmod0vid  14767  lmodvs0  14769  lcomf  14774  lmodvnegcl  14775  lmodvnegid  14776  lmodvsubadd  14785  lmodsubid  14794  lss1d  14830  lspval  14837  ellspsn6  14855  lspsnneg  14867  sralmod  14897  dflidl2rng  14928  lidlacl  14931  dflidl2  14935  df2idl2  14956  qusmul2  14976  quscrng  14980  cnfldmulg  15023  znf1o  15096  znidom  15102  aspval  15125  asclghm  15135  issubassa2  15145  gsumbagdiagfi  15181  psrass1filem  15182  psraddcl  15189  psrmulvalfi  15193  psr0lid  15197  psrlidmfi  15204  tgss3  15316  clsval  15349  clsss3  15368  neiss2  15380  resttop  15408  resttopon2  15416  lmconst  15454  cnima  15458  cnntri  15462  cncnp  15468  cnrest  15473  cndis  15479  lmss  15484  lmff  15487  lmtopcnp  15488  txcnp  15509  upxp  15510  uptx  15512  cnmpt11  15521  hmeoima  15548  hmeoopn  15549  hmeocld  15550  hmeontr  15551  hmeoimaf1o  15552  mettri2  15600  met0  15602  metres2  15619  blpnf  15638  xblss2ps  15642  xblss2  15643  blbas  15671  blres  15672  xmetec  15675  mopnss  15688  xmstri2  15708  mstri2  15709  xmstri  15710  mstri  15711  xmstri3  15712  mstri3  15713  msrtri  15714  mopni3  15722  unimopn  15724  comet  15737  bdxmet  15739  climcncf  15822  dedekindeulemuub  15855  dedekindicclemuub  15864  ivthdichlem  15889  dvfgg  15926  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvfre  15948  dvmptfsum  15963  plyadd  15989  plymul  15990  reeff1olem  16009  reeff1o  16011  sinperlem  16047  abssinper  16085  reexplog  16113  relogexp  16114  cxpexpnn  16141  cxprec  16155  rpcxpmul2  16158  abscxp  16162  wilthlem1  16244  ppival2g  16262  sgmval2  16265  sgmnncl  16269  0sgmppw  16299  chtublem  16307  perfectlem1  16311  bposlem3  16325  bposlem5  16327  bposlem6  16328  lgsdir  16371  lgsprme0  16378  lgsdinn0  16384  gausslemma2dlem3  16399  gausslemma2dlem5a  16401  2lgslem1a2  16423  2lgslem1a  16424  2lgslem3  16437  2lgs  16440  umgredgprv  16573  umgrislfupgrdom  16589  uspgredgiedg  16636  uspgriedgedg  16637  usgrislfuspgrdom  16648  usgredg2en  16653  usgredgprv  16654  usgrpredgv  16656  usgredg  16658  usgrnloopv  16659  usgredgne  16662  usgredg3  16672  usgredgedg  16685  usgredgdomord  16688  usgr1vr  16706  subgruhgrfun  16726  subupgr  16731  subumgr  16732  subusgr  16733  umgrwlknloop  16826  wlkres  16837  clwwlkccatlem  16858  clwwlkccat  16859  depindlem1  16964  depindlem2  16965  depindlem3  16966  bj-inex  17150  bj-nn0suc  17207  bj-nn0sucALT  17221  trilpolemeq1  17308  trilpolemlt1  17309  trirec0  17312  nconstwlpolemgt0  17333