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  596  syl2an2r  597  orandc  945  mp3an3an  1377  eqeqan12d  2245  sylan9eq  2282  csbcomg  3148  sylan9ss  3238  ssconb  3338  ineqan12d  3408  dfopg  3858  breqan12d  4102  opexg  4318  copsex2g  4336  ordin  4480  onin  4481  unexg  4538  eusv1  4547  opelvvg  4773  opthprc  4775  opbrop  4803  relop  4878  dmpropg  5207  unixpm  5270  funssres  5366  funinsn  5376  funtp  5380  fnco  5437  resasplitss  5513  fodmrnu  5564  relrnfvex  5653  funopdmsn  5829  fconst2g  5864  oveqan12d  6032  ovi3  6154  ovg  6156  f1opw2  6224  off  6243  offres  6292  iunon  6445  nnsucsssuc  6655  nnaword1  6676  ertr  6712  erex  6721  brecop  6789  ecovdi  6810  ecovidi  6811  mapvalg  6822  pmvalg  6823  pmss12g  6839  mapsn  6854  en2sn  6983  xpf1o  7025  xpen  7026  phplem4  7036  ssfilem  7057  ssfilemd  7059  diffitest  7071  en1eqsn  7141  sbthlem7  7156  ordiso  7229  updjud  7275  fodju0  7340  finnum  7381  pr2nelem  7390  djucomen  7424  exmidontriimlem1  7429  2onetap  7467  ltsopi  7533  pitric  7534  pitri3or  7535  ltdcpi  7536  mulclpi  7541  addcompig  7542  mulcompig  7544  distrpig  7546  ltexpi  7550  ltapig  7551  ltmpig  7552  dfplpq2  7567  dfmpq2  7568  enqbreq2  7570  enqdc  7574  addcmpblnq  7580  addpipqqslem  7582  mulpipq2  7584  mulpipq  7585  mulpipqqs  7586  addclnq  7588  distrnqg  7600  ltdcnq  7610  ltrnqg  7633  enq0breq  7649  addclnq0  7664  nqnq0a  7667  nqnq0m  7668  nq0m0r  7669  distrnq0  7672  mulcomnq0  7673  genipv  7722  genplt2i  7723  genpelvl  7725  genpelvu  7726  addnqprlemrl  7770  addnqprlemru  7771  addnqprlemfl  7772  addnqprlemfu  7773  addnqpr  7774  mulnqprlemrl  7786  mulnqprlemru  7787  mulnqprlemfl  7788  mulnqprlemfu  7789  mulnqpr  7790  distrlem4prl  7797  distrlem4pru  7798  ltnqpr  7806  recexprlemloc  7844  archrecnq  7876  mulclsr  7967  1idsr  7981  00sr  7982  prsradd  7999  axmulass  8086  axdistr  8087  axcnre  8094  peano5nnnn  8105  mulrid  8169  axltadd  8242  lenlt  8248  cnegexlem3  8349  cnegex  8350  resubcl  8436  subeqrev  8548  muladd  8556  mulsub  8573  mulsub2  8574  ltaddsub2  8610  leaddsub2  8612  leltadd  8620  ltaddpos2  8626  posdif  8628  addge02  8646  mullt0  8653  recexre  8751  recextlem1  8824  recexap  8826  divmuldivap  8885  conjmulap  8902  div2subap  9010  prodgt02  9026  prodge02  9028  lemul2  9030  lemul2a  9032  ltmulgt12  9038  lemulge12  9040  ltmuldiv2  9048  ltdivmul2  9051  ledivmul2  9053  lemuldiv2  9055  negiso  9128  cju  9134  peano5nni  9139  nnaddcl  9156  nnmulcl  9157  nnsub  9175  addltmul  9374  avgle1  9378  avgle2  9379  nnrecl  9393  nn0nnaddcl  9426  zsubcl  9513  zleloe  9519  znnsub  9524  nzadd  9525  zmulcl  9526  zltp1le  9527  zleltp1  9528  nnleltp1  9532  nnltp1le  9533  nnaddm1cl  9534  nn0ltp1le  9535  nn0leltp1  9536  nn0ltlem1  9537  znn0sub  9538  nn0sub  9539  elz2  9544  zapne  9547  zdcle  9549  zdclt  9550  zltlen  9551  nn0lem1lt  9556  nnlem1lt  9557  nnltlem1  9558  zdiv  9561  zextle  9564  zextlt  9565  btwnnz  9567  prime  9572  nneo  9576  peano2uz2  9580  peano5uzti  9581  uzind  9584  fzind  9588  fnn0ind  9589  uzneg  9768  uz11  9772  eluzp1m1  9773  eluzp1p1  9775  uzin  9782  indstr  9820  uz2mulcl  9835  qre  9852  qaddcl  9862  qsubcl  9865  qltlen  9867  qlttri2  9868  irradd  9873  elpqb  9877  cnref1o  9878  rpaddcl  9905  rpmulcl  9906  rpdivcl  9907  rexadd  10080  rexsub  10081  xaddcom  10089  xnn0xadd0  10095  xnegdi  10096  elicc2  10166  iccshftr  10222  iccshftl  10224  iccdil  10226  icccntr  10228  fzval2  10239  elfz1eq  10263  peano2fzr  10265  fznlem  10269  fzsplit2  10278  fzaddel  10287  fzsubel  10288  fzrev2  10313  fzrev3  10315  uzsplit  10320  fzrevral  10333  fzrevral3  10335  fzshftral  10336  elfz2nn0  10340  fznn0sub2  10356  fz0fzdiffz0  10358  elfzmlbp  10360  difelfzle  10362  difelfznle  10363  1fv  10367  elfzouz2  10390  fzo0n  10396  fzouzsplit  10409  fzoun  10411  elfzo0le  10417  fzonmapblen  10419  fzofzim  10420  fzoaddel2  10428  eluzgtdifelfzo  10435  elfzodifsumelfzo  10439  ubmelm1fzo  10464  fzofzp1b  10466  fzosplitprm1  10473  fzostep1  10476  subfzo0  10481  zsupcllemstep  10482  qdclt  10498  qbtwnxr  10510  flqbi2  10544  divfl0  10549  flqzadd  10551  flqmulnn0  10552  addmodidr  10628  modfzo0difsn  10650  frec2uzltd  10658  frec2uzrand  10660  frecfzen2  10682  seqshft2g  10737  seq3split  10743  seqsplitg  10744  seq3caopr2  10748  seqcaopr2g  10749  seqf1oglem2  10775  exp3vallem  10795  expcllem  10805  expcl2lemap  10806  1exp  10823  expge1  10831  expadd  10836  expmul  10839  expsubap  10842  leexp1a  10849  lt2sq  10868  le2sq  10869  sumsqeq0  10873  qsqeqor  10905  bernneq  10915  bernneq2  10916  sq11ap  10962  facdiv  10993  faclbnd  10996  faclbnd3  10998  faclbnd6  10999  facavg  11001  bcrpcl  11008  bccmpl  11009  fiubm  11085  seq3coll  11099  eqwrd  11147  ccatcl  11163  ccatclab  11164  ccatlen  11165  ccat0  11166  ccatval1  11167  ccatval2  11168  elfzelfzccat  11170  ccatvalfn  11171  ccatsymb  11172  ccatval21sw  11175  ccatrn  11179  lswccatn0lsw  11181  ccatalpha  11183  ccatrcl1  11184  swrdfv2  11237  swrdsbslen  11240  swrdspsleq  11241  swrdccat2  11245  pfxclz  11253  ccatpfx  11275  pfxccat1  11276  swrdswrdlem  11278  pfxswrd  11280  pfxccatin12lem4  11300  pfxccatin12lem1  11302  pfxccatin12lem2  11305  pfxccatin12lem3  11306  pfxccat3  11308  swrdccat  11309  pfxccatpfx2  11311  pfxccat3a  11312  swrdccat3blem  11313  swrdccat3b  11314  s2dmg  11364  shftfvalg  11372  shftf  11384  crre  11411  crim  11412  mulreap  11418  readd  11423  resub  11424  remul2  11427  imadd  11431  imsub  11432  immul2  11434  ipcnval  11440  cjsub  11446  cjreim  11457  caucvgre  11535  rexanuz  11542  rexuz3  11544  resqrexlemover  11564  resqrexlemcvg  11573  resqrexlemglsq  11576  sqrtle  11590  sqrtlt  11591  sqrt11ap  11592  sqrt11  11593  absreimsq  11621  absreim  11622  absmul  11623  sqabs  11636  absdiflt  11646  absdifle  11647  abssuble0  11657  abs2difabs  11662  fzomaxdif  11667  caubnd2  11671  rpmaxcl  11777  zmaxcl  11778  nn0maxcl  11779  minmax  11784  mincl  11785  min1inf  11786  min2inf  11787  minabs  11790  minclpr  11791  rpmincl  11792  2zinfmin  11797  xrmaxrecl  11809  xrminmax  11819  xrmincl  11820  xrmin1inf  11821  xrmin2inf  11822  xrminrecl  11827  xrminrpcl  11828  iooinsup  11831  climconst2  11845  climuni  11847  2clim  11855  climshft  11858  climshft2  11860  cjcn2  11870  climaddc1  11883  climmulc2  11885  climsubc1  11886  climsubc2  11887  climlec2  11895  summodclem2a  11935  zsumdc  11938  isumclim3  11977  mptfzshft  11996  fsumrev  11997  fisum0diag2  12001  telfsumo2  12021  fsumparts  12024  cvgcmpub  12030  binomlem  12037  binom1p  12039  binom1dif  12041  bcxmas  12043  isumshft  12044  expcnvap0  12056  expcnv  12058  geosergap  12060  geolim  12065  cvgratnnlemrate  12084  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  prodmodc  12132  zproddc  12133  fprodf1o  12142  fprodeq0  12171  efcj  12227  eftlub  12244  effsumlt  12246  efieq  12289  sinsub  12294  cossub  12295  subsin  12297  sinmul  12298  cosmul  12299  addcos  12300  subcos  12301  dvdssub2  12389  dvdsadd  12390  dvdsaddr  12391  dvdssub  12392  dvdssubr  12393  fzocongeq  12412  odd2np1  12427  opoe  12449  omoe  12450  opeo  12451  omeo  12452  divalgb  12479  ndvdsadd  12485  bitsfi  12511  gcdmndc  12519  gcdabs  12552  dvdsgcd  12576  absmulgcd  12581  gcdmultiple  12584  gcdmultiplez  12585  rpmulgcd  12590  sqgcd  12593  dvdssqlem  12594  dvdssq  12595  nninfctlemfo  12604  nn0seqcvgd  12606  ialgrlemconst  12608  algrf  12610  algrp1  12611  algcvg  12613  algcvga  12616  lcmval  12628  lcmabs  12641  lcmgcd  12643  lcmdvds  12644  lcmgcdnn  12647  coprmgcdb  12653  coprmdvds  12657  coprmdvds2  12658  qredeq  12661  isprm3  12683  nprm  12688  divgcdodd  12708  prmdvdsexp  12713  sqrt2irr  12727  zgcdsq  12766  hashdvds  12786  phiprmpw  12787  crth  12789  phimullem  12790  modprm0  12820  coprimeprodsq  12823  coprimeprodsq2  12824  pythagtriplem2  12832  pythagtriplem19  12848  pcdvdsb  12886  pcneg  12891  pc2dvds  12896  pc11  12897  pcmpt  12909  pcfac  12916  infpnlem1  12925  prmunb  12928  1arithlem4  12932  1arith  12933  gzaddcl  12943  gzmulcl  12944  gzreim  12945  gzsubcl  12946  4sqlem1  12954  4sqlem4a  12957  4sqlem4  12958  4sqlem12  12968  setsvalg  13105  setsfun0  13111  restval  13321  xpsval  13428  mndinvmod  13521  resmhm  13563  resmhm2  13564  mhmco  13566  dfgrp3m  13675  mhmmnd  13696  mulgnngsum  13707  mulgnn0z  13729  mulgnndir  13731  ghmex  13835  0ghm  13838  resghm  13840  resghm2  13841  ghmco  13844  ghmeql  13847  kerf1ghm  13854  ablsubsub23  13905  dfrhm2  14161  isrhm  14165  rhmfn  14179  rhmval  14180  rhmco  14181  resrhm  14255  rhmeql  14257  rhmima  14258  lmodfopne  14333  lspf  14396  znidom  14664  znrrg  14667  innei  14880  cnovex  14913  txuni2  14973  txbasex  14974  txbas  14975  txtop  14977  txtopon  14979  txss12  14983  txbasval  14984  txcnp  14988  upxp  14989  txcnmpt  14990  uptx  14991  txcn  14992  txrest  14993  txdis  14994  cnmpt21  15008  hmeoco  15033  txhmeo  15036  isxmet2d  15065  blin2  15149  comet  15216  metcn  15231  txmetcn  15236  qtopbasss  15238  qtopbas  15239  remetdval  15264  bl2ioo  15267  blssioo  15270  divcnap  15282  cncfmet  15309  dvaddxxbr  15418  dvcjbr  15425  plyf  15454  ply1termlem  15459  plymullem1  15465  plyaddlem  15466  plymullem  15467  plycolemc  15475  plyreres  15481  dvply1  15482  efle  15493  reapef  15495  sinperlem  15525  sincosq2sgn  15544  sincosq3sgn  15545  sincos6thpi  15559  ioocosf1o  15571  relogoprlem  15585  logleb  15592  cxple3  15638  cxpcom  15655  dvdsppwf1o  15706  fsumdvdsmul  15708  1sgmprm  15711  mersenne  15714  lgslem3  15724  lgsdir2  15755  lgsdir  15757  lgsdilem2  15758  lgsdi  15759  gausslemma2dlem1a  15780  gausslemma2dlem3  15785  gausslemma2dlem6  15789  lgseisenlem3  15794  lgseisenlem4  15795  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2  15805  lgsquad3  15806  2lgslem1a1  15808  2lgslem1a  15810  2lgslem1c  15812  2sqlem2  15837  mul2sq  15838  2sqlem7  15843  usgredg2v  16068  ushgredgedg  16070  ushgredgedgloop  16072  vtxedgfi  16100  vtxlpfi  16101  wlkeq  16165  uspgr2wlkeq  16176  clwwlkccatlem  16209  clwwlkccat  16210  clwwlknccat  16232  bj-inex  16452  bj-bdfindis  16492  triap  16583  cvgcmp2nlemabs  16586  trilpolemisumle  16592  inffz  16626