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  4214  otexg  4370  opelopabt  4404  sonr  4462  sotr  4463  issod  4464  so2nr  4466  so3nr  4467  ordelss  4524  onelon  4529  elrnmpt1s  5032  iota2  5367  funeu  5402  imadif  5461  fnbr  5485  feu  5574  f1ss  5604  f1ssres  5607  f1resf1  5608  dffo2  5619  foco  5626  foun  5658  fun11iun  5660  ffoss  5672  funbrfv  5739  fvco3  5776  fvopab6  5805  funfvbrb  5822  elpreima  5828  ffvelcdm  5841  ffvelcdmda  5843  dffo4  5856  fmptco  5874  fsn2  5882  fncofn  5893  fvconst2g  5929  fex  5947  funfvima  5950  f1elima  5979  f1ocnvfv1  5983  f1ocnvfv2  5984  cocan2  5994  foeqcnvco  5996  isocnv  6017  isores2  6019  isoini  6024  isoselem  6026  f1oiso  6032  f1ofveu  6073  eloprabga  6175  suppssof1  6320  ofco  6321  offveqb  6322  ofc1g  6324  ofc2g  6325  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  fnexALT  6340  f1dmex  6345  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  eqopi  6406  2ndrn  6417  fo2ndf  6463  suppval1  6479  ressuppss  6494  suppssrst  6501  suppssrgst  6502  smores3  6564  smores2  6565  smoel  6571  smoiso  6573  tfrlem1  6579  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemiubacc  6601  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfr1onlemubacc  6617  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcllemubacc  6630  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  frecrdg  6679  omv2  6738  nnasuc  6749  nnmsuc  6750  nnacom  6757  nnaass  6758  nnmass  6760  nntri1  6769  nndifsnid  6780  nnmordi  6789  swoer  6835  erth  6853  riinerm  6882  qliftlem  6887  ecovass  6918  ecoviass  6919  elmapssres  6954  fvixp  6985  f1domg  7044  domssr  7064  endomtr  7077  xpsnen2g  7127  enen1  7140  enen2  7141  domen1  7142  domen2  7143  mapen  7146  mapxpen  7148  ssenen  7152  phplem1  7153  fidifsnid  7173  findcard  7192  findcard2  7193  findcard2s  7194  fidcen  7203  fieq0  7310  isotilem  7347  supisolem  7349  inflbti  7365  ordiso2  7376  djuex  7384  updjudhcoinlf  7421  updjudhcoinrg  7422  updjud  7423  ctssdccl  7452  enumctlemm  7455  nnnninf  7467  finomni  7481  pm54.43  7537  acfun  7564  ccfunen  7631  cc2lem  7633  cc3  7635  addclpi  7695  addasspig  7698  mulasspig  7700  addnidpig  7704  nnppipi  7711  ltanqi  7770  ltmnqi  7771  ltexnqq  7776  archnqq  7785  prarloclemarch2  7787  enq0sym  7800  enq0tr  7802  nqnq0pi  7806  nqnq0  7809  mulcanenq0ec  7813  addclnq0  7819  nqpnq0nq  7821  distrnq0  7827  addassnq0lemcl  7829  addassnq0  7830  prubl  7854  prarloclemlt  7861  genpdf  7876  genipv  7877  genpelvl  7880  genpelvu  7881  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  genpassl  7892  genpassu  7893  genpassg  7894  addnqprl  7897  addnqpru  7898  addlocpr  7904  nqprm  7910  nqprl  7919  nqpru  7920  mulnqprl  7936  mulnqpru  7937  mullocprlem  7938  mullocpr  7939  addcomprg  7946  mulcomprg  7948  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  ltprordil  7957  1idprl  7958  1idpru  7959  ltpopr  7963  ltsopr  7964  ltaddpr  7965  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  prplnqu  7988  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  aptiprleml  8007  aptiprlemu  8008  cauappcvgprlemloc  8020  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemloc  8043  caucvgprlemladdrl  8046  caucvgprprlemml  8062  caucvgprprlemloc  8071  00sr  8137  map2psrprg  8173  suplocsrlempr  8175  suplocsrlem  8176  adddir  8318  axsuploc  8399  eqle  8418  le2tri3i  8436  mul4  8460  muladd11  8461  cnegexlem3  8505  addsub12  8541  2addsub  8542  addsubeq4  8543  subadd4  8572  negcon1  8580  negdi2  8586  negsubdi2  8587  neg2sub  8588  renegcl  8589  muladd  8713  subdir  8715  gt0ne0  8757  ltnegcon1  8793  lenegcon1  8796  eqord1  8813  eqord2  8814  recexre  8909  ltmul1  8923  recexap  8984  div12ap  9027  rerecapb  9176  p1le  9182  ltmul2  9189  gt0div  9203  ge0div  9204  zlem1lt  9706  nnaddm1cl  9711  zdceq  9725  gtndiv  9746  prime  9750  msqznn  9751  btwnz  9770  uzss  9953  eluzadd  9961  nn0pzuz  9997  supinfneg  10005  infsupneg  10006  divfnzn  10031  qnegcl  10046  qreccl  10052  elpqb  10061  xaddass  10282  xleadd1a  10286  xlesubadd  10296  elico2  10350  iccss  10354  iccsupr  10379  elfz5  10431  fznn  10507  difelfznle  10553  fzoaddel  10616  elincfzoext  10622  qdceq  10690  qbtwnxr  10703  flqbi2  10740  adddivflid  10741  fldivnn0  10744  divfl0  10745  flqmulnn0  10748  fldivnn0le  10752  fldiv4p1lem1div2  10754  ceiqle  10764  flqdiv  10772  modqmulnn  10793  frecuzrdgtcl  10863  frecuzrdgsuc  10865  frecuzrdgdomlem  10868  frecuzrdgfunlem  10870  frecuzrdgsuctlem  10874  seqm1g  10925  seq3caopr2  10944  seqcaopr2g  10945  iseqf1olemkle  10948  seq3f1olemp  10966  seqf1oglem2  10971  seqf1og  10972  seq3id  10976  seq3z  10979  expap0  11020  mulexp  11029  mulexpzap  11030  expmul  11035  leexp1a  11045  expubnd  11047  zesq  11110  bernneq  11112  bernneq3  11114  modqexp  11118  facdiv  11191  facndiv  11192  faclbnd3  11196  faclbnd6  11197  bccmpl  11207  bcpasc  11219  bccl  11220  hashfibclem  11297  hashfibc  11298  seq3coll  11309  fundm2domnop  11316  wrdsymb1  11356  ccatfv0  11386  ccatrn  11392  ccat2s1cl  11416  lswccats1fst  11427  swrdspsleq  11454  pfxtrcfv  11480  pfxsuffeqwrdeq  11485  pfxlswccat  11500  wrdeqs1cat  11507  cats1un  11508  swrdccatin1  11512  pfxccatin12lem4  11513  swrdccatin2  11516  pfxccatin12  11520  swrdccat  11522  shftlem  11596  ovshftex  11599  shftval4  11608  shftf  11610  shftcan2  11615  crim  11638  mulreap  11644  remul2  11653  immul2  11660  cjexp  11673  caucvgre  11762  r19.2uz  11774  sqrtsq2  11824  absnid  11854  absexp  11861  nn0abscl  11867  abslt  11870  lenegsq  11877  cau3lem  11896  minmax  12013  xrmaxadd  12045  clim  12065  climshftlemg  12086  climcn1  12092  climcn1lem  12103  clim2ser  12121  clim2ser2  12122  iserex  12123  isermulc2  12124  climub  12128  climcaucn  12135  serf0  12136  summodclem3  12165  summodclem2a  12166  summodclem2  12167  summodc  12168  fsum3  12172  fsumf1o  12175  fisumss  12177  isumss2  12178  fsumcl2lem  12183  fsumadd  12191  fsumsplit  12192  isummulc2  12211  fsum2d  12220  fsummulc2  12233  telfsumo  12251  fsumparts  12255  hash2iun1dif1  12265  bcxmas  12274  isumshft  12275  isumsplit  12276  expcnvap0  12287  geolim  12296  geolim2  12297  cvgratnnlemmn  12310  cvgratnnlemseq  12311  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  clim2divap  12325  prodmodclem3  12360  prodmodclem2a  12361  fprodseq  12368  fprodf1o  12373  fprodmul  12376  fprodsplitdc  12381  efcllemp  12443  reefcl  12453  efcj  12458  efaddlem  12459  efexp  12467  reeftlcl  12474  eftlub  12475  efsep  12476  effsumlt  12477  eflegeo  12486  retanclap  12507  demoivre  12558  demoivreALT  12559  eirraplem  12562  dvdsval3  12576  p1modz1  12579  iddvdsexp  12600  alzdvds  12639  addmodlteqALT  12644  nnehalf  12689  nno  12691  ndvdsadd  12716  bitsp1e  12737  bitsp1o  12738  bitsinv1  12747  divgcdnnr  12771  neggcd  12778  gcdabs  12783  bezoutlemmain  12793  bezoutlemaz  12798  bezoutlembz  12799  gcdmultiplez  12816  gcdzeq  12817  dvdssq  12826  nninfctlemfo  12835  algrf  12841  algcvg  12844  algcvga  12847  algfx  12848  eucalgf  12851  eucalgcvga  12854  neglcm  12871  lcmabs  12872  lcmdvds  12875  lcmgcdeq  12879  qredeq  12892  isprm3  12914  coprm  12941  prmrp  12942  isprm6  12944  prmdvdsexpb  12946  rpexp  12950  cncongrprm  12954  sqrt2irraplemnn  12977  phibndlem  13016  phiprmpw  13022  eulerthlemh  13031  eulerthlemth  13032  fermltl  13034  prmdivdiv  13037  modprm1div  13048  m1dvdsndvds  13049  coprimeprodsq  13058  pczpre  13098  pczcl  13099  pcexp  13110  pczdvds  13115  pczndvds  13117  pczndvds2  13119  pcdvdsb  13121  pcneg  13126  pcprmpw  13135  difsqpwdvds  13139  pcmptcl  13143  pcprod  13147  fldivp1  13149  infpnlem2  13161  1arithlem4  13167  prmlem0  13242  ballotfilem2  13279  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemfrcn0  13324  ennnfonelemrn  13361  topnidg  13657  imasaddfnlemg  13686  imasaddflemg  13688  qusin  13698  mgmlrid  13750  mndass  13788  mhmco  13848  gzsumwcl  13853  gzsumwmhm  13854  grpass  13865  grpinvex  13866  dfgrp2  13883  grplid  13887  grprid  13888  grprcan  13893  grpinvssd  13933  grpinvval2  13939  mhmid  13969  mhmmnd  13970  ghmgrp  13972  mulgnn  13980  mulgnnp1  13984  mulgnegnn  13986  mulgnnsubcl  13988  mulgz  14004  issubg2m  14043  issubg4m  14047  subgintm  14052  nmzbi  14063  eqger  14078  eqgid  14080  eqgen  14081  qusgrp  14086  qusadd  14088  qusinv  14090  qussub  14091  ghminv  14104  ghmsub  14105  ghmrn  14111  resghm2b  14116  ghmf1  14127  conjsubg  14131  conjsubgen  14132  qusghm  14136  cmncom  14156  ablsubadd  14167  ablsubsub23  14180  ghmcmn  14182  gzsumreidx  14192  gsumsubmfi  14219  prdsidlem  14244  prdsinvlem  14247  pwselbasb  14257  pwsplusgval  14259  pwsmulrval  14260  pwsinvg  14266  mgpress  14281  srg1expzeq1  14350  ringinvnz1ne0  14405  ringinvnzdiv  14406  dvdsrd  14452  dvdsunit  14470  unitinvcl  14481  unitinvinv  14482  unitlinv  14484  unitrinv  14485  rhmunitinv  14536  subrngintm  14571  subrg1  14590  subrguss  14595  subrginv  14596  subrgunit  14598  subrgugrp  14599  subrgintm  14602  resrhm  14607  resrhm2b  14608  lmodass  14690  lmodlcan  14691  lmod0vlid  14706  lmod0vrid  14707  lmod0vid  14708  lmodvs0  14710  lcomf  14715  lmodvnegcl  14716  lmodvnegid  14717  lmodvsubadd  14726  lmodsubid  14735  lss1d  14771  lspval  14778  ellspsn6  14796  lspsnneg  14808  sralmod  14838  dflidl2rng  14869  lidlacl  14872  dflidl2  14876  df2idl2  14897  qusmul2  14917  quscrng  14921  cnfldmulg  14964  znf1o  15037  znidom  15043  aspval  15066  asclghm  15076  issubassa2  15086  psraddcl  15123  psr0lid  15125  tgss3  15231  clsval  15264  clsss3  15283  neiss2  15295  resttop  15323  resttopon2  15331  lmconst  15369  cnima  15373  cnntri  15377  cncnp  15383  cnrest  15388  cndis  15394  lmss  15399  lmff  15402  lmtopcnp  15403  txcnp  15424  upxp  15425  uptx  15427  cnmpt11  15436  hmeoima  15463  hmeoopn  15464  hmeocld  15465  hmeontr  15466  hmeoimaf1o  15467  mettri2  15515  met0  15517  metres2  15534  blpnf  15553  xblss2ps  15557  xblss2  15558  blbas  15586  blres  15587  xmetec  15590  mopnss  15603  xmstri2  15623  mstri2  15624  xmstri  15625  mstri  15626  xmstri3  15627  mstri3  15628  msrtri  15629  mopni3  15637  unimopn  15639  comet  15652  bdxmet  15654  climcncf  15737  dedekindeulemuub  15770  dedekindicclemuub  15779  ivthdichlem  15804  dvfgg  15841  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvfre  15863  dvmptfsum  15878  plyadd  15904  plymul  15905  reeff1olem  15924  reeff1o  15926  sinperlem  15962  abssinper  16000  reexplog  16026  relogexp  16027  cxpexpnn  16054  cxprec  16068  rpcxpmul2  16071  abscxp  16073  wilthlem1  16154  ppival2g  16172  sgmval2  16175  sgmnncl  16179  0sgmppw  16209  chtublem  16217  perfectlem1  16221  bposlem3  16235  bposlem5  16237  lgsdir  16276  lgsprme0  16283  lgsdinn0  16289  gausslemma2dlem3  16304  gausslemma2dlem5a  16306  2lgslem1a2  16328  2lgslem1a  16329  2lgslem3  16342  2lgs  16345  umgredgprv  16478  umgrislfupgrdom  16494  uspgredgiedg  16541  uspgriedgedg  16542  usgrislfuspgrdom  16553  usgredg2en  16558  usgredgprv  16559  usgrpredgv  16561  usgredg  16563  usgrnloopv  16564  usgredgne  16567  usgredg3  16577  usgredgedg  16590  usgredgdomord  16593  usgr1vr  16611  subgruhgrfun  16631  subupgr  16636  subumgr  16637  subusgr  16638  umgrwlknloop  16731  wlkres  16742  clwwlkccatlem  16763  clwwlkccat  16764  depindlem1  16869  depindlem2  16870  depindlem3  16871  bj-inex  17055  bj-nn0suc  17112  bj-nn0sucALT  17126  trilpolemeq1  17211  trilpolemlt1  17212  trirec0  17215  nconstwlpolemgt0  17236