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  571  pm4.55dc  947  dfifp2dc  990  3adantl1  1180  3adantl2  1181  3adantl3  1182  syl3anl1  1322  syl3anl3  1324  syl3anl  1325  stoic3  1476  eupick  2162  csbiebt  3181  csbnestgf  3194  reuss2  3505  mpteq12  4198  otexg  4351  opelopabt  4385  sonr  4443  sotr  4444  issod  4445  so2nr  4447  so3nr  4448  ordelss  4505  onelon  4510  elrnmpt1s  5012  iota2  5347  funeu  5382  imadif  5441  fnbr  5465  feu  5554  f1ss  5584  f1ssres  5587  f1resf1  5588  dffo2  5599  foco  5606  foun  5638  fun11iun  5640  ffoss  5652  funbrfv  5718  fvco3  5753  fvopab6  5779  funfvbrb  5796  elpreima  5802  ffvelcdm  5815  ffvelcdmda  5817  dffo4  5830  fmptco  5848  fsn2  5856  fncofn  5867  fvconst2g  5903  fex  5920  funfvima  5923  f1elima  5952  f1ocnvfv1  5956  f1ocnvfv2  5957  cocan2  5967  foeqcnvco  5969  isocnv  5990  isores2  5992  isoini  5997  isoselem  5999  f1oiso  6005  f1ofveu  6046  eloprabga  6148  suppssof1  6293  ofco  6294  offveqb  6295  ofc1g  6297  ofc2g  6298  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  fnexALT  6313  f1dmex  6318  ot1stg  6359  ot2ndg  6360  ot3rdgg  6361  eqopi  6379  2ndrn  6390  fo2ndf  6436  suppval1  6452  ressuppss  6467  suppssrst  6474  suppssrgst  6475  smores3  6537  smores2  6538  smoel  6544  smoiso  6546  tfrlem1  6552  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemiubacc  6574  tfr1onlemsucaccv  6585  tfr1onlembfn  6588  tfr1onlemubacc  6590  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembfn  6601  tfrcllemubacc  6603  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  frecrdg  6652  omv2  6711  nnasuc  6722  nnmsuc  6723  nnacom  6730  nnaass  6731  nnmass  6733  nntri1  6742  nndifsnid  6753  nnmordi  6762  swoer  6808  erth  6826  riinerm  6855  qliftlem  6860  ecovass  6891  ecoviass  6892  elmapssres  6920  fvixp  6951  f1domg  7010  domssr  7030  endomtr  7043  xpsnen2g  7093  enen1  7106  enen2  7107  domen1  7108  domen2  7109  mapen  7112  mapxpen  7114  ssenen  7118  phplem1  7119  fidifsnid  7139  findcard  7158  findcard2  7159  findcard2s  7160  fidcen  7169  fieq0  7276  isotilem  7310  supisolem  7312  inflbti  7328  ordiso2  7339  djuex  7347  updjudhcoinlf  7384  updjudhcoinrg  7385  updjud  7386  ctssdccl  7415  enumctlemm  7418  nnnninf  7430  finomni  7444  pm54.43  7500  acfun  7527  ccfunen  7594  cc2lem  7596  cc3  7598  addclpi  7658  addasspig  7661  mulasspig  7663  addnidpig  7667  nnppipi  7674  ltanqi  7733  ltmnqi  7734  ltexnqq  7739  archnqq  7748  prarloclemarch2  7750  enq0sym  7763  enq0tr  7765  nqnq0pi  7769  nqnq0  7772  mulcanenq0ec  7776  addclnq0  7782  nqpnq0nq  7784  distrnq0  7790  addassnq0lemcl  7792  addassnq0  7793  prubl  7817  prarloclemlt  7824  genpdf  7839  genipv  7840  genpelvl  7843  genpelvu  7844  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpassl  7855  genpassu  7856  genpassg  7857  addnqprl  7860  addnqpru  7861  addlocpr  7867  nqprm  7873  nqprl  7882  nqpru  7883  mulnqprl  7899  mulnqpru  7900  mullocprlem  7901  mullocpr  7902  addcomprg  7909  mulcomprg  7911  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  1idprl  7921  1idpru  7922  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  prplnqu  7951  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  aptiprleml  7970  aptiprlemu  7971  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemloc  8006  caucvgprlemladdrl  8009  caucvgprprlemml  8025  caucvgprprlemloc  8034  00sr  8100  map2psrprg  8136  suplocsrlempr  8138  suplocsrlem  8139  adddir  8281  axsuploc  8362  eqle  8381  le2tri3i  8398  mul4  8421  muladd11  8422  cnegexlem3  8466  addsub12  8502  2addsub  8503  addsubeq4  8504  subadd4  8533  negcon1  8541  negdi2  8547  negsubdi2  8548  neg2sub  8549  renegcl  8550  muladd  8674  subdir  8676  gt0ne0  8718  ltnegcon1  8754  lenegcon1  8757  eqord1  8774  eqord2  8775  recexre  8869  ltmul1  8883  recexap  8944  div12ap  8985  rerecapb  9134  p1le  9140  ltmul2  9147  gt0div  9161  ge0div  9162  zlem1lt  9651  nnaddm1cl  9656  zdceq  9670  gtndiv  9691  prime  9695  msqznn  9696  btwnz  9715  uzss  9893  eluzadd  9901  nn0pzuz  9937  supinfneg  9945  infsupneg  9946  divfnzn  9971  qnegcl  9986  qreccl  9992  elpqb  10000  xaddass  10221  xleadd1a  10225  xlesubadd  10235  elico2  10289  iccss  10293  iccsupr  10318  elfz5  10370  fznn  10445  difelfznle  10491  fzoaddel  10554  elincfzoext  10560  qdceq  10628  qbtwnxr  10641  flqbi2  10675  adddivflid  10676  fldivnn0  10679  divfl0  10680  flqmulnn0  10683  fldivnn0le  10687  fldiv4p1lem1div2  10689  ceiqle  10699  flqdiv  10707  modqmulnn  10728  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgdomlem  10803  frecuzrdgfunlem  10805  frecuzrdgsuctlem  10809  seqm1g  10860  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemkle  10883  seq3f1olemp  10901  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3z  10914  expap0  10955  mulexp  10964  mulexpzap  10965  expmul  10970  leexp1a  10980  expubnd  10982  zesq  11045  bernneq  11047  bernneq3  11049  modqexp  11053  facdiv  11125  facndiv  11126  faclbnd3  11130  faclbnd6  11131  bccmpl  11141  bcpasc  11153  bccl  11154  hashfibclem  11231  hashfibc  11232  seq3coll  11239  fundm2domnop  11246  wrdsymb1  11286  ccatfv0  11316  ccatrn  11322  ccat2s1cl  11346  lswccats1fst  11357  swrdspsleq  11384  pfxtrcfv  11410  pfxsuffeqwrdeq  11415  pfxlswccat  11430  wrdeqs1cat  11437  cats1un  11438  swrdccatin1  11442  pfxccatin12lem4  11443  swrdccatin2  11446  pfxccatin12  11450  swrdccat  11452  shftlem  11526  ovshftex  11529  shftval4  11538  shftf  11540  shftcan2  11545  crim  11568  mulreap  11574  remul2  11583  immul2  11590  cjexp  11603  caucvgre  11691  r19.2uz  11703  sqrtsq2  11753  absnid  11783  absexp  11789  nn0abscl  11795  abslt  11798  lenegsq  11805  cau3lem  11824  minmax  11940  xrmaxadd  11971  clim  11991  climshftlemg  12012  climcn1  12018  climcn1lem  12029  clim2ser  12047  clim2ser2  12048  iserex  12049  isermulc2  12050  climub  12054  climcaucn  12061  serf0  12062  summodclem3  12091  summodclem2a  12092  summodclem2  12093  summodc  12094  fsum3  12098  fsumf1o  12101  fisumss  12103  isumss2  12104  fsumcl2lem  12109  fsumadd  12117  fsumsplit  12118  isummulc2  12137  fsum2d  12146  fsummulc2  12159  telfsumo  12177  fsumparts  12181  hash2iun1dif1  12191  bcxmas  12200  isumshft  12201  isumsplit  12202  expcnvap0  12213  geolim  12222  geolim2  12223  cvgratnnlemmn  12236  cvgratnnlemseq  12237  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2divap  12251  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodf1o  12299  fprodmul  12302  fprodsplitdc  12307  efcllemp  12369  reefcl  12379  efcj  12384  efaddlem  12385  efexp  12393  reeftlcl  12400  eftlub  12401  efsep  12402  effsumlt  12403  eflegeo  12412  retanclap  12433  demoivre  12484  demoivreALT  12485  eirraplem  12488  dvdsval3  12502  p1modz1  12505  iddvdsexp  12526  alzdvds  12565  addmodlteqALT  12570  nnehalf  12615  nno  12617  ndvdsadd  12642  bitsp1e  12663  bitsp1o  12664  bitsinv1  12673  divgcdnnr  12697  neggcd  12704  gcdabs  12709  bezoutlemmain  12719  bezoutlemaz  12724  bezoutlembz  12725  gcdmultiplez  12742  gcdzeq  12743  dvdssq  12752  nninfctlemfo  12761  algrf  12767  algcvg  12770  algcvga  12773  algfx  12774  eucalgf  12777  eucalgcvga  12780  neglcm  12797  lcmabs  12798  lcmdvds  12801  lcmgcdeq  12805  qredeq  12818  isprm3  12840  coprm  12866  prmrp  12867  isprm6  12869  prmdvdsexpb  12871  rpexp  12875  cncongrprm  12879  sqrt2irraplemnn  12901  phibndlem  12938  phiprmpw  12944  eulerthlemh  12953  eulerthlemth  12954  fermltl  12956  prmdivdiv  12959  modprm1div  12970  m1dvdsndvds  12971  coprimeprodsq  12980  pczpre  13020  pczcl  13021  pcexp  13032  pczdvds  13037  pczndvds  13039  pczndvds2  13041  pcdvdsb  13043  pcneg  13048  pcprmpw  13057  difsqpwdvds  13061  pcmptcl  13065  pcprod  13069  fldivp1  13071  infpnlem2  13083  1arithlem4  13089  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfrcn0  13217  ennnfonelemrn  13254  topnidg  13549  pwselbasb  13590  pwsplusgval  13592  pwsmulrval  13593  imasaddfnlemg  13611  imasaddflemg  13613  qusin  13623  mgmlrid  13676  mndass  13721  prdsidlem  13744  mhmco  13787  gsumsubm  13791  gsumwcl  13794  gsumwmhm  13795  grpass  13806  grpinvex  13807  dfgrp2  13824  grplid  13828  grprid  13829  grprcan  13834  grpinvssd  13874  grpinvval2  13880  prdsinvlem  13905  pwsinvg  13909  mhmid  13916  mhmmnd  13917  ghmgrp  13919  mulgnn  13927  mulgnnp1  13931  mulgnegnn  13933  mulgnnsubcl  13935  mulgz  13951  issubg2m  13990  issubg4m  13994  subgintm  13999  nmzbi  14010  eqger  14025  eqgid  14027  eqgen  14028  qusgrp  14033  qusadd  14035  qusinv  14037  qussub  14038  ghminv  14051  ghmsub  14052  ghmrn  14058  resghm2b  14063  ghmf1  14074  conjsubg  14078  conjsubgen  14079  qusghm  14083  cmncom  14103  ablsubadd  14113  ablsubsub23  14126  ghmcmn  14128  gsumfzreidx  14138  mgpress  14159  srg1expzeq1  14223  ringinvnz1ne0  14277  ringinvnzdiv  14278  dvdsrd  14324  dvdsunit  14342  unitinvcl  14353  unitinvinv  14354  unitlinv  14356  unitrinv  14357  rhmunitinv  14408  subrngintm  14443  subrg1  14462  subrguss  14467  subrginv  14468  subrgunit  14470  subrgugrp  14471  subrgintm  14474  resrhm  14479  resrhm2b  14480  lmodass  14563  lmodlcan  14564  lmod0vlid  14578  lmod0vrid  14579  lmod0vid  14580  lmodvs0  14582  lcomf  14587  lmodvnegcl  14588  lmodvnegid  14589  lmodvsubadd  14598  lmodsubid  14607  lss1d  14643  lspval  14650  lspsnel6  14668  lspsnneg  14680  sralmod  14710  dflidl2rng  14741  lidlacl  14744  dflidl2  14748  df2idl2  14769  qusmul2  14789  quscrng  14793  cnfldmulg  14836  znf1o  14911  znidom  14917  psraddcl  14947  psr0lid  14949  tgss3  15055  clsval  15088  clsss3  15107  neiss2  15119  resttop  15147  resttopon2  15155  lmconst  15193  cnima  15197  cnntri  15201  cncnp  15207  cnrest  15212  cndis  15218  lmss  15223  lmff  15226  lmtopcnp  15227  txcnp  15248  upxp  15249  uptx  15251  cnmpt11  15260  hmeoima  15287  hmeoopn  15288  hmeocld  15289  hmeontr  15290  hmeoimaf1o  15291  mettri2  15339  met0  15341  metres2  15358  blpnf  15377  xblss2ps  15381  xblss2  15382  blbas  15410  blres  15411  xmetec  15414  mopnss  15427  xmstri2  15447  mstri2  15448  xmstri  15449  mstri  15450  xmstri3  15451  mstri3  15452  msrtri  15453  mopni3  15461  unimopn  15463  comet  15476  bdxmet  15478  climcncf  15561  dedekindeulemuub  15594  dedekindicclemuub  15603  ivthdichlem  15628  dvfgg  15665  dvidlemap  15668  dvidrelem  15669  dvidsslem  15670  dvfre  15687  dvmptfsum  15702  plyadd  15728  plymul  15729  reeff1olem  15748  reeff1o  15750  sinperlem  15785  abssinper  15823  reexplog  15848  relogexp  15849  cxpexpnn  15873  cxprec  15887  rpcxpmul2  15890  abscxp  15892  wilthlem1  15960  sgmval2  15964  sgmnncl  15968  0sgmppw  15973  perfectlem1  15979  lgsdir  16020  lgsprme0  16027  lgsdinn0  16033  gausslemma2dlem3  16048  gausslemma2dlem5a  16050  2lgslem1a2  16072  2lgslem1a  16073  2lgslem3  16086  2lgs  16089  umgredgprv  16222  umgrislfupgrdom  16238  uspgredgiedg  16285  uspgriedgedg  16286  usgrislfuspgrdom  16297  usgredg2en  16302  usgredgprv  16303  usgrpredgv  16305  usgredg  16307  usgrnloopv  16308  usgredgne  16311  usgredg3  16321  usgredgedg  16334  usgredgdomord  16337  usgr1vr  16355  subgruhgrfun  16375  subupgr  16380  subumgr  16381  subusgr  16382  umgrwlknloop  16475  wlkres  16486  clwwlkccatlem  16507  clwwlkccat  16508  depindlem1  16613  depindlem2  16614  depindlem3  16615  bj-inex  16789  bj-nn0suc  16846  bj-nn0sucALT  16860  trilpolemeq1  16936  trilpolemlt1  16937  trirec0  16940  nconstwlpolemgt0  16962