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  8422  muladd11  8423  cnegexlem3  8467  addsub12  8503  2addsub  8504  addsubeq4  8505  subadd4  8534  negcon1  8542  negdi2  8548  negsubdi2  8549  neg2sub  8550  renegcl  8551  muladd  8675  subdir  8677  gt0ne0  8719  ltnegcon1  8755  lenegcon1  8758  eqord1  8775  eqord2  8776  recexre  8870  ltmul1  8884  recexap  8945  div12ap  8988  rerecapb  9137  p1le  9143  ltmul2  9150  gt0div  9164  ge0div  9165  zlem1lt  9654  nnaddm1cl  9659  zdceq  9673  gtndiv  9694  prime  9698  msqznn  9699  btwnz  9718  uzss  9896  eluzadd  9904  nn0pzuz  9940  supinfneg  9948  infsupneg  9949  divfnzn  9974  qnegcl  9989  qreccl  9995  elpqb  10003  xaddass  10224  xleadd1a  10228  xlesubadd  10238  elico2  10292  iccss  10296  iccsupr  10321  elfz5  10373  fznn  10448  difelfznle  10494  fzoaddel  10557  elincfzoext  10563  qdceq  10631  qbtwnxr  10644  flqbi2  10678  adddivflid  10679  fldivnn0  10682  divfl0  10683  flqmulnn0  10686  fldivnn0le  10690  fldiv4p1lem1div2  10692  ceiqle  10702  flqdiv  10710  modqmulnn  10731  frecuzrdgtcl  10801  frecuzrdgsuc  10803  frecuzrdgdomlem  10806  frecuzrdgfunlem  10808  frecuzrdgsuctlem  10812  seqm1g  10863  seq3caopr2  10882  seqcaopr2g  10883  iseqf1olemkle  10886  seq3f1olemp  10904  seqf1oglem2  10909  seqf1og  10910  seq3id  10914  seq3z  10917  expap0  10958  mulexp  10967  mulexpzap  10968  expmul  10973  leexp1a  10983  expubnd  10985  zesq  11048  bernneq  11050  bernneq3  11052  modqexp  11056  facdiv  11128  facndiv  11129  faclbnd3  11133  faclbnd6  11134  bccmpl  11144  bcpasc  11156  bccl  11157  hashfibclem  11234  hashfibc  11235  seq3coll  11242  fundm2domnop  11249  wrdsymb1  11289  ccatfv0  11319  ccatrn  11325  ccat2s1cl  11349  lswccats1fst  11360  swrdspsleq  11387  pfxtrcfv  11413  pfxsuffeqwrdeq  11418  pfxlswccat  11433  wrdeqs1cat  11440  cats1un  11441  swrdccatin1  11445  pfxccatin12lem4  11446  swrdccatin2  11449  pfxccatin12  11453  swrdccat  11455  shftlem  11529  ovshftex  11532  shftval4  11541  shftf  11543  shftcan2  11548  crim  11571  mulreap  11577  remul2  11586  immul2  11593  cjexp  11606  caucvgre  11695  r19.2uz  11707  sqrtsq2  11757  absnid  11787  absexp  11793  nn0abscl  11799  abslt  11802  lenegsq  11809  cau3lem  11828  minmax  11944  xrmaxadd  11975  clim  11995  climshftlemg  12016  climcn1  12022  climcn1lem  12033  clim2ser  12051  clim2ser2  12052  iserex  12053  isermulc2  12054  climub  12058  climcaucn  12065  serf0  12066  summodclem3  12095  summodclem2a  12096  summodclem2  12097  summodc  12098  fsum3  12102  fsumf1o  12105  fisumss  12107  isumss2  12108  fsumcl2lem  12113  fsumadd  12121  fsumsplit  12122  isummulc2  12141  fsum2d  12150  fsummulc2  12163  telfsumo  12181  fsumparts  12185  hash2iun1dif1  12195  bcxmas  12204  isumshft  12205  isumsplit  12206  expcnvap0  12217  geolim  12226  geolim2  12227  cvgratnnlemmn  12240  cvgratnnlemseq  12241  mertenslemi1  12250  mertenslem2  12251  mertensabs  12252  clim2divap  12255  prodmodclem3  12290  prodmodclem2a  12291  fprodseq  12298  fprodf1o  12303  fprodmul  12306  fprodsplitdc  12311  efcllemp  12373  reefcl  12383  efcj  12388  efaddlem  12389  efexp  12397  reeftlcl  12404  eftlub  12405  efsep  12406  effsumlt  12407  eflegeo  12416  retanclap  12437  demoivre  12488  demoivreALT  12489  eirraplem  12492  dvdsval3  12506  p1modz1  12509  iddvdsexp  12530  alzdvds  12569  addmodlteqALT  12574  nnehalf  12619  nno  12621  ndvdsadd  12646  bitsp1e  12667  bitsp1o  12668  bitsinv1  12677  divgcdnnr  12701  neggcd  12708  gcdabs  12713  bezoutlemmain  12723  bezoutlemaz  12728  bezoutlembz  12729  gcdmultiplez  12746  gcdzeq  12747  dvdssq  12756  nninfctlemfo  12765  algrf  12771  algcvg  12774  algcvga  12777  algfx  12778  eucalgf  12781  eucalgcvga  12784  neglcm  12801  lcmabs  12802  lcmdvds  12805  lcmgcdeq  12809  qredeq  12822  isprm3  12844  coprm  12870  prmrp  12871  isprm6  12873  prmdvdsexpb  12875  rpexp  12879  cncongrprm  12883  sqrt2irraplemnn  12905  phibndlem  12942  phiprmpw  12948  eulerthlemh  12957  eulerthlemth  12958  fermltl  12960  prmdivdiv  12963  modprm1div  12974  m1dvdsndvds  12975  coprimeprodsq  12984  pczpre  13024  pczcl  13025  pcexp  13036  pczdvds  13041  pczndvds  13043  pczndvds2  13045  pcdvdsb  13047  pcneg  13052  pcprmpw  13061  difsqpwdvds  13065  pcmptcl  13069  pcprod  13073  fldivp1  13075  infpnlem2  13087  1arithlem4  13093  ballotfilem2  13176  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemfrcn0  13221  ennnfonelemrn  13258  topnidg  13553  imasaddfnlemg  13582  imasaddflemg  13584  qusin  13594  mgmlrid  13646  mndass  13689  mhmco  13749  gsumsubm  13753  gsumwcl  13756  gsumwmhm  13757  grpass  13768  grpinvex  13769  dfgrp2  13786  grplid  13790  grprid  13791  grprcan  13796  grpinvssd  13836  grpinvval2  13842  mhmid  13872  mhmmnd  13873  ghmgrp  13875  mulgnn  13883  mulgnnp1  13887  mulgnegnn  13889  mulgnnsubcl  13891  mulgz  13907  issubg2m  13946  issubg4m  13950  subgintm  13955  nmzbi  13966  eqger  13981  eqgid  13983  eqgen  13984  qusgrp  13989  qusadd  13991  qusinv  13993  qussub  13994  ghminv  14007  ghmsub  14008  ghmrn  14014  resghm2b  14019  ghmf1  14030  conjsubg  14034  conjsubgen  14035  qusghm  14039  cmncom  14059  ablsubadd  14069  ablsubsub23  14082  ghmcmn  14084  gsumfzreidx  14094  prdsidlem  14139  prdsinvlem  14142  pwselbasb  14152  pwsplusgval  14154  pwsmulrval  14155  pwsinvg  14161  mgpress  14174  srg1expzeq1  14242  ringinvnz1ne0  14296  ringinvnzdiv  14297  dvdsrd  14343  dvdsunit  14361  unitinvcl  14372  unitinvinv  14373  unitlinv  14375  unitrinv  14376  rhmunitinv  14427  subrngintm  14462  subrg1  14481  subrguss  14486  subrginv  14487  subrgunit  14489  subrgugrp  14490  subrgintm  14493  resrhm  14498  resrhm2b  14499  lmodass  14581  lmodlcan  14582  lmod0vlid  14596  lmod0vrid  14597  lmod0vid  14598  lmodvs0  14600  lcomf  14605  lmodvnegcl  14606  lmodvnegid  14607  lmodvsubadd  14616  lmodsubid  14625  lss1d  14661  lspval  14668  lspsnel6  14686  lspsnneg  14698  sralmod  14728  dflidl2rng  14759  lidlacl  14762  dflidl2  14766  df2idl2  14787  qusmul2  14807  quscrng  14811  cnfldmulg  14854  znf1o  14929  znidom  14935  psraddcl  14965  psr0lid  14967  tgss3  15073  clsval  15106  clsss3  15125  neiss2  15137  resttop  15165  resttopon2  15173  lmconst  15211  cnima  15215  cnntri  15219  cncnp  15225  cnrest  15230  cndis  15236  lmss  15241  lmff  15244  lmtopcnp  15245  txcnp  15266  upxp  15267  uptx  15269  cnmpt11  15278  hmeoima  15305  hmeoopn  15306  hmeocld  15307  hmeontr  15308  hmeoimaf1o  15309  mettri2  15357  met0  15359  metres2  15376  blpnf  15395  xblss2ps  15399  xblss2  15400  blbas  15428  blres  15429  xmetec  15432  mopnss  15445  xmstri2  15465  mstri2  15466  xmstri  15467  mstri  15468  xmstri3  15469  mstri3  15470  msrtri  15471  mopni3  15479  unimopn  15481  comet  15494  bdxmet  15496  climcncf  15579  dedekindeulemuub  15612  dedekindicclemuub  15621  ivthdichlem  15646  dvfgg  15683  dvidlemap  15686  dvidrelem  15687  dvidsslem  15688  dvfre  15705  dvmptfsum  15720  plyadd  15746  plymul  15747  reeff1olem  15766  reeff1o  15768  sinperlem  15803  abssinper  15841  reexplog  15866  relogexp  15867  cxpexpnn  15891  cxprec  15905  rpcxpmul2  15908  abscxp  15910  wilthlem1  15978  sgmval2  15982  sgmnncl  15986  0sgmppw  15991  perfectlem1  15997  lgsdir  16038  lgsprme0  16045  lgsdinn0  16051  gausslemma2dlem3  16066  gausslemma2dlem5a  16068  2lgslem1a2  16090  2lgslem1a  16091  2lgslem3  16104  2lgs  16107  umgredgprv  16240  umgrislfupgrdom  16256  uspgredgiedg  16303  uspgriedgedg  16304  usgrislfuspgrdom  16315  usgredg2en  16320  usgredgprv  16321  usgrpredgv  16323  usgredg  16325  usgrnloopv  16326  usgredgne  16329  usgredg3  16339  usgredgedg  16352  usgredgdomord  16355  usgr1vr  16373  subgruhgrfun  16393  subupgr  16398  subumgr  16399  subusgr  16400  umgrwlknloop  16493  wlkres  16504  clwwlkccatlem  16525  clwwlkccat  16526  depindlem1  16631  depindlem2  16632  depindlem3  16633  bj-inex  16817  bj-nn0suc  16874  bj-nn0sucALT  16888  trilpolemeq1  16964  trilpolemlt1  16965  trirec0  16968  nconstwlpolemgt0  16989