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  4167  otexg  4316  opelopabt  4350  sonr  4408  sotr  4409  issod  4410  so2nr  4412  so3nr  4413  ordelss  4470  onelon  4475  elrnmpt1s  4974  iota2  5308  funeu  5343  imadif  5401  fnbr  5425  feu  5510  f1ss  5539  f1ssres  5542  f1resf1  5543  dffo2  5554  foco  5561  foun  5593  fun11iun  5595  ffoss  5606  funbrfv  5672  fvco3  5707  fvopab6  5733  funfvbrb  5750  elpreima  5756  ffvelcdm  5770  ffvelcdmda  5772  dffo4  5785  fmptco  5803  fsn2  5811  fncofn  5821  fvconst2g  5857  fex  5872  funfvima  5875  f1elima  5903  f1ocnvfv1  5907  f1ocnvfv2  5908  cocan2  5918  foeqcnvco  5920  isocnv  5941  isores2  5943  isoini  5948  isoselem  5950  f1oiso  5956  f1ofveu  5995  eloprabga  6097  suppssof1  6242  ofco  6243  offveqb  6244  ofc1g  6246  ofc2g  6247  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  fnexALT  6262  f1dmex  6267  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  eqopi  6324  2ndrn  6335  fo2ndf  6379  smores3  6445  smores2  6446  smoel  6452  smoiso  6454  tfrlem1  6460  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemiubacc  6482  tfr1onlemsucaccv  6493  tfr1onlembfn  6496  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembfn  6509  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  frecrdg  6560  omv2  6619  nnasuc  6630  nnmsuc  6631  nnacom  6638  nnaass  6639  nnmass  6641  nntri1  6650  nndifsnid  6661  nnmordi  6670  swoer  6716  erth  6734  riinerm  6763  qliftlem  6768  ecovass  6799  ecoviass  6800  elmapssres  6828  fvixp  6858  f1domg  6917  domssr  6937  endomtr  6950  xpsnen2g  6996  enen1  7009  enen2  7010  domen1  7011  domen2  7012  mapen  7015  mapxpen  7017  ssenen  7020  phplem1  7021  fidifsnid  7041  findcard  7058  findcard2  7059  findcard2s  7060  fieq0  7151  isotilem  7181  supisolem  7183  inflbti  7199  ordiso2  7210  djuex  7218  updjudhcoinlf  7255  updjudhcoinrg  7256  updjud  7257  ctssdccl  7286  enumctlemm  7289  nnnninf  7301  finomni  7315  pm54.43  7371  acfun  7397  ccfunen  7458  cc2lem  7460  cc3  7462  addclpi  7522  addasspig  7525  mulasspig  7527  addnidpig  7531  nnppipi  7538  ltanqi  7597  ltmnqi  7598  ltexnqq  7603  archnqq  7612  prarloclemarch2  7614  enq0sym  7627  enq0tr  7629  nqnq0pi  7633  nqnq0  7636  mulcanenq0ec  7640  addclnq0  7646  nqpnq0nq  7648  distrnq0  7654  addassnq0lemcl  7656  addassnq0  7657  prubl  7681  prarloclemlt  7688  genpdf  7703  genipv  7704  genpelvl  7707  genpelvu  7708  genpml  7712  genpmu  7713  genprndl  7716  genprndu  7717  genpassl  7719  genpassu  7720  genpassg  7721  addnqprl  7724  addnqpru  7725  addlocpr  7731  nqprm  7737  nqprl  7746  nqpru  7747  mulnqprl  7763  mulnqpru  7764  mullocprlem  7765  mullocpr  7766  addcomprg  7773  mulcomprg  7775  distrlem1prl  7777  distrlem1pru  7778  distrlem4prl  7779  distrlem4pru  7780  ltprordil  7784  1idprl  7785  1idpru  7786  ltpopr  7790  ltsopr  7791  ltaddpr  7792  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemdisj  7801  ltexprlemloc  7802  ltexprlemfl  7804  ltexprlemrl  7805  ltexprlemfu  7806  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  prplnqu  7815  recexprlemloc  7826  recexprlem1ssl  7828  recexprlem1ssu  7829  recexprlemss1l  7830  recexprlemss1u  7831  aptiprleml  7834  aptiprlemu  7835  cauappcvgprlemloc  7847  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemloc  7870  caucvgprlemladdrl  7873  caucvgprprlemml  7889  caucvgprprlemloc  7898  00sr  7964  map2psrprg  8000  suplocsrlempr  8002  suplocsrlem  8003  adddir  8145  axsuploc  8227  eqle  8246  le2tri3i  8263  mul4  8286  muladd11  8287  cnegexlem3  8331  addsub12  8367  2addsub  8368  addsubeq4  8369  subadd4  8398  negcon1  8406  negdi2  8412  negsubdi2  8413  neg2sub  8414  renegcl  8415  muladd  8538  subdir  8540  gt0ne0  8582  ltnegcon1  8618  lenegcon1  8621  eqord1  8638  eqord2  8639  recexre  8733  ltmul1  8747  recexap  8808  div12ap  8849  rerecapb  8998  p1le  9004  ltmul2  9011  gt0div  9025  ge0div  9026  zlem1lt  9511  nnaddm1cl  9516  zdceq  9530  gtndiv  9550  prime  9554  msqznn  9555  btwnz  9574  uzss  9751  eluzadd  9759  nn0pzuz  9790  supinfneg  9798  infsupneg  9799  divfnzn  9824  qnegcl  9839  qreccl  9845  elpqb  9853  xaddass  10073  xleadd1a  10077  xlesubadd  10087  elico2  10141  iccss  10145  iccsupr  10170  elfz5  10221  fznn  10293  difelfznle  10339  fzoaddel  10401  elincfzoext  10407  qdceq  10472  qbtwnxr  10485  flqbi2  10519  adddivflid  10520  fldivnn0  10523  divfl0  10524  flqmulnn0  10527  fldivnn0le  10531  fldiv4p1lem1div2  10533  ceiqle  10543  flqdiv  10551  modqmulnn  10572  frecuzrdgtcl  10642  frecuzrdgsuc  10644  frecuzrdgdomlem  10647  frecuzrdgfunlem  10649  frecuzrdgsuctlem  10653  seqm1g  10704  seq3caopr2  10723  seqcaopr2g  10724  iseqf1olemkle  10727  seq3f1olemp  10745  seqf1oglem2  10750  seqf1og  10751  seq3id  10755  seq3z  10758  expap0  10799  mulexp  10808  mulexpzap  10809  expmul  10814  leexp1a  10824  expubnd  10826  zesq  10888  bernneq  10890  bernneq3  10892  modqexp  10896  facdiv  10968  facndiv  10969  faclbnd3  10973  faclbnd6  10974  bccmpl  10984  bcpasc  10996  bccl  10997  seq3coll  11072  fundm2domnop  11076  wrdsymb1  11116  ccatfv0  11146  ccatrn  11152  ccat2s1cl  11174  lswccats1fst  11183  swrdspsleq  11207  pfxtrcfv  11233  pfxsuffeqwrdeq  11238  pfxlswccat  11253  wrdeqs1cat  11260  cats1un  11261  swrdccatin1  11265  pfxccatin12lem4  11266  swrdccatin2  11269  pfxccatin12  11273  swrdccat  11275  shftlem  11335  ovshftex  11338  shftval4  11347  shftf  11349  shftcan2  11354  crim  11377  mulreap  11383  remul2  11392  immul2  11399  cjexp  11412  caucvgre  11500  r19.2uz  11512  sqrtsq2  11562  absnid  11592  absexp  11598  nn0abscl  11604  abslt  11607  lenegsq  11614  cau3lem  11633  minmax  11749  xrmaxadd  11780  clim  11800  climshftlemg  11821  climcn1  11827  climcn1lem  11838  clim2ser  11856  clim2ser2  11857  iserex  11858  isermulc2  11859  climub  11863  climcaucn  11870  serf0  11871  summodclem3  11899  summodclem2a  11900  summodclem2  11901  summodc  11902  fsum3  11906  fsumf1o  11909  fisumss  11911  isumss2  11912  fsumcl2lem  11917  fsumadd  11925  fsumsplit  11926  isummulc2  11945  fsum2d  11954  fsummulc2  11967  telfsumo  11985  fsumparts  11989  hash2iun1dif1  11999  bcxmas  12008  isumshft  12009  isumsplit  12010  expcnvap0  12021  geolim  12030  geolim2  12031  cvgratnnlemmn  12044  cvgratnnlemseq  12045  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  clim2divap  12059  prodmodclem3  12094  prodmodclem2a  12095  fprodseq  12102  fprodf1o  12107  fprodmul  12110  fprodsplitdc  12115  efcllemp  12177  reefcl  12187  efcj  12192  efaddlem  12193  efexp  12201  reeftlcl  12208  eftlub  12209  efsep  12210  effsumlt  12211  eflegeo  12220  retanclap  12241  demoivre  12292  demoivreALT  12293  eirraplem  12296  dvdsval3  12310  p1modz1  12313  iddvdsexp  12334  alzdvds  12373  addmodlteqALT  12378  nnehalf  12423  nno  12425  ndvdsadd  12450  bitsp1e  12471  bitsp1o  12472  bitsinv1  12481  divgcdnnr  12505  neggcd  12512  gcdabs  12517  bezoutlemmain  12527  bezoutlemaz  12532  bezoutlembz  12533  gcdmultiplez  12550  gcdzeq  12551  dvdssq  12560  nninfctlemfo  12569  algrf  12575  algcvg  12578  algcvga  12581  algfx  12582  eucalgf  12585  eucalgcvga  12588  neglcm  12605  lcmabs  12606  lcmdvds  12609  lcmgcdeq  12613  qredeq  12626  isprm3  12648  coprm  12674  prmrp  12675  isprm6  12677  prmdvdsexpb  12679  rpexp  12683  cncongrprm  12687  sqrt2irraplemnn  12709  phibndlem  12746  phiprmpw  12752  eulerthlemh  12761  eulerthlemth  12762  fermltl  12764  prmdivdiv  12767  modprm1div  12778  m1dvdsndvds  12779  coprimeprodsq  12788  pczpre  12828  pczcl  12829  pcexp  12840  pczdvds  12845  pczndvds  12847  pczndvds2  12849  pcdvdsb  12851  pcneg  12856  pcprmpw  12865  difsqpwdvds  12869  pcmptcl  12873  pcprod  12877  fldivp1  12879  infpnlem2  12891  1arithlem4  12897  ennnfonelemrn  12998  topnidg  13293  pwselbasb  13334  pwsplusgval  13336  pwsmulrval  13337  imasaddfnlemg  13355  imasaddflemg  13357  qusin  13367  mgmlrid  13420  mndass  13465  prdsidlem  13488  mhmco  13531  gsumsubm  13535  gsumwcl  13538  gsumwmhm  13539  grpass  13550  grpinvex  13551  dfgrp2  13568  grplid  13572  grprid  13573  grprcan  13578  grpinvssd  13618  grpinvval2  13624  prdsinvlem  13649  pwsinvg  13653  mhmid  13660  mhmmnd  13661  ghmgrp  13663  mulgnn  13671  mulgnnp1  13675  mulgnegnn  13677  mulgnnsubcl  13679  mulgz  13695  issubg2m  13734  issubg4m  13738  subgintm  13743  nmzbi  13754  eqger  13769  eqgid  13771  eqgen  13772  qusgrp  13777  qusadd  13779  qusinv  13781  qussub  13782  ghminv  13795  ghmsub  13796  ghmrn  13802  resghm2b  13807  ghmf1  13818  conjsubg  13822  conjsubgen  13823  qusghm  13827  cmncom  13847  ablsubadd  13857  ablsubsub23  13870  ghmcmn  13872  gsumfzreidx  13882  mgpress  13902  srg1expzeq1  13966  ringinvnz1ne0  14020  ringinvnzdiv  14021  dvdsrd  14066  dvdsunit  14084  unitinvcl  14095  unitinvinv  14096  unitlinv  14098  unitrinv  14099  rhmunitinv  14150  subrngintm  14184  subrg1  14203  subrguss  14208  subrginv  14209  subrgunit  14211  subrgugrp  14212  subrgintm  14215  resrhm  14220  resrhm2b  14221  lmodass  14275  lmodlcan  14276  lmod0vlid  14290  lmod0vrid  14291  lmod0vid  14292  lmodvs0  14294  lcomf  14299  lmodvnegcl  14300  lmodvnegid  14301  lmodvsubadd  14310  lmodsubid  14319  lss1d  14355  lspval  14362  lspsnel6  14380  lspsnneg  14392  sralmod  14422  dflidl2rng  14453  lidlacl  14456  dflidl2  14460  df2idl2  14481  qusmul2  14501  quscrng  14505  cnfldmulg  14548  znf1o  14623  znidom  14629  psraddcl  14652  psr0lid  14654  tgss3  14760  clsval  14793  clsss3  14812  neiss2  14824  resttop  14852  resttopon2  14860  lmconst  14898  cnima  14902  cnntri  14906  cncnp  14912  cnrest  14917  cndis  14923  lmss  14928  lmff  14931  lmtopcnp  14932  txcnp  14953  upxp  14954  uptx  14956  cnmpt11  14965  hmeoima  14992  hmeoopn  14993  hmeocld  14994  hmeontr  14995  hmeoimaf1o  14996  mettri2  15044  met0  15046  metres2  15063  blpnf  15082  xblss2ps  15086  xblss2  15087  blbas  15115  blres  15116  xmetec  15119  mopnss  15132  xmstri2  15152  mstri2  15153  xmstri  15154  mstri  15155  xmstri3  15156  mstri3  15157  msrtri  15158  mopni3  15166  unimopn  15168  comet  15181  bdxmet  15183  climcncf  15266  dedekindeulemuub  15299  dedekindicclemuub  15308  ivthdichlem  15333  dvfgg  15370  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvfre  15392  dvmptfsum  15407  plyadd  15433  plymul  15434  reeff1olem  15453  reeff1o  15455  sinperlem  15490  abssinper  15528  reexplog  15553  relogexp  15554  cxpexpnn  15578  cxprec  15592  rpcxpmul2  15595  abscxp  15597  wilthlem1  15662  sgmval2  15666  sgmnncl  15670  0sgmppw  15675  perfectlem1  15681  lgsdir  15722  lgsprme0  15729  lgsdinn0  15735  gausslemma2dlem3  15750  gausslemma2dlem5a  15752  2lgslem1a2  15774  2lgslem1a  15775  2lgslem3  15788  2lgs  15791  umgredgprv  15923  umgrislfupgrdom  15937  uspgredgiedg  15984  uspgriedgedg  15985  usgrislfuspgrdom  15996  usgredg2en  16001  usgredgprv  16002  usgrpredgv  16004  usgredg  16006  usgrnloopv  16007  usgredgne  16010  usgredg3  16020  usgredgedg  16033  usgredgdomord  16036  umgrwlknloop  16089  wlkres  16098  bj-inex  16294  bj-nn0suc  16351  bj-nn0sucALT  16365  fidcen  16379  trilpolemeq1  16438  trilpolemlt1  16439  trirec0  16442  nconstwlpolemgt0  16462