Theorem syl2an 289

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2an	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 ⊢ (𝜏 → 𝜒)
2		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 283	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 286	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:  syl2anr  290  anim12i  338  syl2an2  598  syl2an2r  599  orandc  948  mp3an3an  1380  eqeqan12d  2250  sylan9eq  2287  csbcomg  3164  sylan9ss  3255  ssconb  3356  ineqan12d  3428  dfopg  3886  breqan12d  4130  opexg  4349  copsex2g  4367  ordin  4511  onin  4512  unexg  4569  eusv1  4578  opelvvg  4804  opthprc  4806  opbrop  4834  relop  4910  dmpropg  5240  unixpm  5303  funssres  5400  funinsn  5410  funtp  5414  fnco  5471  resasplitss  5549  fodmrnu  5603  relrnfvex  5693  funopdmsn  5869  fconst2g  5904  oveqan12d  6077  ovi3  6199  ovg  6201  f1opw2  6269  off  6288  offres  6341  suppfnss  6470  iunon  6528  nnsucsssuc  6738  nnaword1  6759  ertr  6795  erex  6804  brecop  6872  ecovdi  6893  ecovidi  6894  mapvalg  6905  pmvalg  6906  pmss12g  6922  mapsn  6938  en2sn  7068  xpf1o  7110  xpen  7111  phplem4  7122  ssfilem  7143  ssfilemd  7145  diffitest  7157  en1eqsn  7231  sbthlem7  7246  fsuppxpfi  7262  ordiso  7340  updjud  7386  fodju0  7451  finnum  7492  pr2nelem  7501  djucomen  7536  exmidontriimlem1  7541  2onetap  7585  ltsopi  7651  pitric  7652  pitri3or  7653  ltdcpi  7654  mulclpi  7659  addcompig  7660  mulcompig  7662  distrpig  7664  ltexpi  7668  ltapig  7669  ltmpig  7670  dfplpq2  7685  dfmpq2  7686  enqbreq2  7688  enqdc  7692  addcmpblnq  7698  addpipqqslem  7700  mulpipq2  7702  mulpipq  7703  mulpipqqs  7704  addclnq  7706  distrnqg  7718  ltdcnq  7728  ltrnqg  7751  enq0breq  7767  addclnq0  7782  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  distrnq0  7790  mulcomnq0  7791  genipv  7840  genplt2i  7841  genpelvl  7843  genpelvu  7844  addnqprlemrl  7888  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  addnqpr  7892  mulnqprlemrl  7904  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  mulnqpr  7908  distrlem4prl  7915  distrlem4pru  7916  ltnqpr  7924  recexprlemloc  7962  archrecnq  7994  mulclsr  8085  1idsr  8099  00sr  8100  prsradd  8117  axmulass  8204  axdistr  8205  axcnre  8212  peano5nnnn  8223  mulrid  8287  axltadd  8359  lenlt  8365  cnegexlem3  8467  cnegex  8468  resubcl  8554  subeqrev  8666  muladd  8675  mulsub  8692  mulsub2  8693  ltaddsub2  8729  leaddsub2  8731  leltadd  8739  ltaddpos2  8745  posdif  8747  addge02  8765  mullt0  8772  recexre  8870  recextlem1  8943  recexap  8945  divmuldivap  9006  conjmulap  9023  div2subap  9131  prodgt02  9147  prodge02  9149  lemul2  9151  lemul2a  9153  ltmulgt12  9159  lemulge12  9161  ltmuldiv2  9169  ltdivmul2  9172  ledivmul2  9174  lemuldiv2  9176  negiso  9249  cju  9255  peano5nni  9260  nnaddcl  9277  nnmulcl  9278  nnsub  9296  addltmul  9495  avgle1  9499  avgle2  9500  nnrecl  9514  nn0nnaddcl  9547  zsubcl  9638  zleloe  9644  znnsub  9649  nzadd  9650  zmulcl  9651  zltp1le  9652  zleltp1  9653  nnleltp1  9657  nnltp1le  9658  nnaddm1cl  9659  nn0ltp1le  9660  nn0leltp1  9661  nn0ltlem1  9662  znn0sub  9663  nn0sub  9664  elz2  9669  zapne  9672  zdcle  9674  zdclt  9675  zltlen  9677  nn0lem1lt  9682  nnlem1lt  9683  nnltlem1  9684  zdiv  9687  zextle  9690  zextlt  9691  btwnnz  9693  prime  9698  nneo  9702  peano2uz2  9706  peano5uzti  9707  uzind  9710  fzind  9714  fnn0ind  9715  uzneg  9894  uz11  9898  eluzp1m1  9899  eluzp1p1  9901  uzin  9908  indstr  9946  uz2mulcl  9961  qre  9978  qaddcl  9988  qsubcl  9991  qltlen  9993  qlttri2  9994  irradd  9999  elpqb  10003  cnref1o  10004  rpaddcl  10031  rpmulcl  10032  rpdivcl  10033  rexadd  10207  rexsub  10208  xaddcom  10216  xnn0xadd0  10222  xnegdi  10223  elicc2  10293  iccshftr  10349  iccshftl  10351  iccdil  10353  icccntr  10355  fzval2  10367  elfz1eq  10392  peano2fzr  10394  fznlem  10398  fzsplit2  10407  fzsplit3  10410  fzaddel  10417  fzsubel  10418  fzrev2  10444  fzrev3  10446  uzsplit  10451  fzrevral  10464  fzrevral3  10466  fzshftral  10467  elfz2nn0  10471  fznn0sub2  10487  fz0fzdiffz0  10489  elfzmlbp  10491  difelfzle  10493  difelfznle  10494  1fv  10498  elfzouz2  10521  fzo0n  10527  fzouzsplit  10540  fzoun  10542  elfzo0le  10549  fzonmapblen  10551  fzofzim  10552  fzoaddel2  10560  eluzgtdifelfzo  10567  elfzodifsumelfzo  10571  ubmelm1fzo  10596  fzofzp1b  10598  fzosplitprm1  10605  fzostep1  10608  subfzo0  10613  zsupcllemstep  10614  qdclt  10632  qbtwnxr  10644  flqbi2  10678  divfl0  10683  flqzadd  10685  flqmulnn0  10686  addmodidr  10762  modfzo0difsn  10784  frec2uzltd  10792  frec2uzrand  10794  frecfzen2  10816  seqshft2g  10871  seq3split  10877  seqsplitg  10878  seq3caopr2  10882  seqcaopr2g  10883  seqf1oglem2  10909  exp3vallem  10929  expcllem  10939  expcl2lemap  10940  1exp  10957  expge1  10965  expadd  10970  expmul  10973  expsubap  10976  leexp1a  10983  lt2sq  11002  le2sq  11003  sumsqeq0  11007  qsqeqor  11039  bernneq  11050  bernneq2  11051  sq11ap  11097  facdiv  11128  faclbnd  11131  faclbnd3  11133  faclbnd6  11134  facavg  11136  bcrpcl  11143  bccmpl  11144  bcm1n  11159  fiubm  11223  seq3coll  11242  eqwrd  11293  ccatcl  11309  ccatclab  11310  ccatlen  11311  ccat0  11312  ccatval1  11313  ccatval2  11314  elfzelfzccat  11316  ccatvalfn  11317  ccatsymb  11318  ccatval21sw  11321  ccatrn  11325  lswccatn0lsw  11327  ccatalpha  11329  ccatrcl1  11330  swrdfv2  11383  swrdsbslen  11386  swrdspsleq  11387  swrdccat2  11391  pfxclz  11399  ccatpfx  11421  pfxccat1  11422  swrdswrdlem  11424  pfxswrd  11426  pfxccatin12lem4  11446  pfxccatin12lem1  11448  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccat3  11454  swrdccat  11455  pfxccatpfx2  11457  pfxccat3a  11458  swrdccat3blem  11459  swrdccat3b  11460  s2dmg  11510  shftfvalg  11531  shftf  11543  crre  11570  crim  11571  mulreap  11577  readd  11582  resub  11583  remul2  11586  imadd  11590  imsub  11591  immul2  11593  ipcnval  11599  cjsub  11605  cjreim  11616  caucvgre  11694  rexanuz  11701  rexuz3  11703  resqrexlemover  11723  resqrexlemcvg  11732  resqrexlemglsq  11735  sqrtle  11749  sqrtlt  11750  sqrt11ap  11751  sqrt11  11752  absreimsq  11780  absreim  11781  absmul  11782  sqabs  11795  absdiflt  11805  absdifle  11806  abssuble0  11816  abs2difabs  11821  fzomaxdif  11826  caubnd2  11830  rpmaxcl  11936  zmaxcl  11937  nn0maxcl  11938  minmax  11943  mincl  11944  min1inf  11945  min2inf  11946  minabs  11949  minclpr  11950  rpmincl  11951  2zinfmin  11956  xrmaxrecl  11968  xrminmax  11978  xrmincl  11979  xrmin1inf  11980  xrmin2inf  11981  xrminrecl  11986  xrminrpcl  11987  iooinsup  11990  climconst2  12004  climuni  12006  2clim  12014  climshft  12017  climshft2  12019  cjcn2  12029  climaddc1  12042  climmulc2  12044  climsubc1  12045  climsubc2  12046  climlec2  12054  summodclem2a  12095  zsumdc  12098  isumclim3  12137  mptfzshft  12156  fsumrev  12157  fisum0diag2  12161  telfsumo2  12181  fsumparts  12184  cvgcmpub  12190  binomlem  12197  binom1p  12199  binom1dif  12201  bcxmas  12203  isumshft  12204  expcnvap0  12216  expcnv  12218  geosergap  12220  geolim  12225  cvgratnnlemrate  12244  mertenslemi1  12249  mertenslem2  12250  mertensabs  12251  prodmodc  12292  zproddc  12293  fprodf1o  12302  fprodeq0  12331  efcj  12387  eftlub  12404  effsumlt  12406  efieq  12449  sinsub  12454  cossub  12455  subsin  12457  sinmul  12458  cosmul  12459  addcos  12460  subcos  12461  dvdssub2  12549  dvdsadd  12550  dvdsaddr  12551  dvdssub  12552  dvdssubr  12553  fzocongeq  12572  odd2np1  12587  opoe  12609  omoe  12610  opeo  12611  omeo  12612  divalgb  12639  ndvdsadd  12645  bitsfi  12671  gcdmndc  12679  gcdabs  12712  dvdsgcd  12736  absmulgcd  12741  gcdmultiple  12744  gcdmultiplez  12745  rpmulgcd  12750  sqgcd  12753  dvdssqlem  12754  dvdssq  12755  nninfctlemfo  12764  nn0seqcvgd  12766  ialgrlemconst  12768  algrf  12770  algrp1  12771  algcvg  12773  algcvga  12776  lcmval  12788  lcmabs  12801  lcmgcd  12803  lcmdvds  12804  lcmgcdnn  12807  coprmgcdb  12813  coprmdvds  12817  coprmdvds2  12818  qredeq  12821  isprm3  12843  nprm  12848  divgcdodd  12868  prmdvdsexp  12873  sqrt2irr  12887  zgcdsq  12926  hashdvds  12946  phiprmpw  12947  crth  12949  phimullem  12950  modprm0  12980  coprimeprodsq  12983  coprimeprodsq2  12984  pythagtriplem2  12992  pythagtriplem19  13008  pcdvdsb  13046  pcneg  13051  pc2dvds  13056  pc11  13057  pcmpt  13069  pcfac  13076  infpnlem1  13085  prmunb  13088  1arithlem4  13092  1arith  13093  gzaddcl  13103  gzmulcl  13104  gzreim  13105  gzsubcl  13106  4sqlem1  13114  4sqlem4a  13117  4sqlem4  13118  4sqlem12  13128  ballotfilemfc0  13179  ballotfilemfcc  13180  setsvalg  13329  setsfun0  13335  restval  13545  mndinvmod  13709  resmhm  13745  resmhm2  13746  mhmco  13748  dfgrp3m  13857  mhmmnd  13872  mulgnngsum  13883  mulgnn0z  13905  mulgnndir  13907  ghmex  14011  0ghm  14014  resghm  14016  resghm2  14017  ghmco  14020  ghmeql  14023  kerf1ghm  14030  ablsubsub23  14081  xpsval  14146  dfrhm2  14402  isrhm  14406  rhmfn  14420  rhmval  14421  rhmco  14422  resrhm  14497  rhmeql  14499  rhmima  14500  lmodfopne  14603  lspf  14666  znidom  14934  znrrg  14937  innei  15157  cnovex  15190  txuni2  15250  txbasex  15251  txbas  15252  txtop  15254  txtopon  15256  txss12  15260  txbasval  15261  txcnp  15265  upxp  15266  txcnmpt  15267  uptx  15268  txcn  15269  txrest  15270  txdis  15271  cnmpt21  15285  hmeoco  15310  txhmeo  15313  isxmet2d  15342  blin2  15426  comet  15493  metcn  15508  txmetcn  15513  qtopbasss  15515  qtopbas  15516  remetdval  15541  bl2ioo  15544  blssioo  15547  divcnap  15559  cncfmet  15586  dvaddxxbr  15695  dvcjbr  15702  plyf  15731  ply1termlem  15736  plymullem1  15742  plyaddlem  15743  plymullem  15744  plycolemc  15752  plyreres  15758  dvply1  15759  efle  15770  reapef  15772  sinperlem  15802  sincosq2sgn  15821  sincosq3sgn  15822  sincos6thpi  15836  ioocosf1o  15848  relogoprlem  15862  logleb  15869  cxple3  15915  cxpcom  15932  dvdsppwf1o  15986  fsumdvdsmul  15988  1sgmprm  15991  mersenne  15994  lgslem3  16004  lgsdir2  16035  lgsdir  16037  lgsdilem2  16038  lgsdi  16039  gausslemma2dlem1a  16060  gausslemma2dlem3  16065  gausslemma2dlem6  16069  lgseisenlem3  16074  lgseisenlem4  16075  lgsquadlem1  16079  lgsquadlem2  16080  lgsquad2  16085  lgsquad3  16086  2lgslem1a1  16088  2lgslem1a  16090  2lgslem1c  16092  2sqlem2  16117  mul2sq  16118  2sqlem7  16123  usgredg2v  16348  ushgredgedg  16350  ushgredgedgloop  16352  uhgrissubgr  16385  vtxedgfi  16413  vtxlpfi  16414  wlkeq  16478  uspgr2wlkeq  16489  clwwlkccatlem  16524  clwwlkccat  16525  clwwlknccat  16547  bj-inex  16816  bj-bdfindis  16856  triap  16952  cvgcmp2nlemabs  16955  trilpolemisumle  16961  inffz  16997