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  3147  sylan9ss  3237  ssconb  3337  ineqan12d  3407  dfopg  3855  breqan12d  4099  opexg  4315  copsex2g  4333  ordin  4477  onin  4478  unexg  4535  eusv1  4544  opelvvg  4770  opthprc  4772  opbrop  4800  relop  4875  dmpropg  5204  unixpm  5267  funssres  5363  funinsn  5373  funtp  5377  fnco  5434  resasplitss  5510  fodmrnu  5561  relrnfvex  5650  funopdmsn  5826  fconst2g  5861  oveqan12d  6029  ovi3  6151  ovg  6153  f1opw2  6221  off  6240  offres  6289  iunon  6441  nnsucsssuc  6651  nnaword1  6672  ertr  6708  erex  6717  brecop  6785  ecovdi  6806  ecovidi  6807  mapvalg  6818  pmvalg  6819  pmss12g  6835  mapsn  6850  en2sn  6979  xpf1o  7018  xpen  7019  phplem4  7029  ssfilem  7050  diffitest  7062  en1eqsn  7131  sbthlem7  7146  ordiso  7219  updjud  7265  fodju0  7330  finnum  7371  pr2nelem  7380  djucomen  7414  exmidontriimlem1  7419  2onetap  7457  ltsopi  7523  pitric  7524  pitri3or  7525  ltdcpi  7526  mulclpi  7531  addcompig  7532  mulcompig  7534  distrpig  7536  ltexpi  7540  ltapig  7541  ltmpig  7542  dfplpq2  7557  dfmpq2  7558  enqbreq2  7560  enqdc  7564  addcmpblnq  7570  addpipqqslem  7572  mulpipq2  7574  mulpipq  7575  mulpipqqs  7576  addclnq  7578  distrnqg  7590  ltdcnq  7600  ltrnqg  7623  enq0breq  7639  addclnq0  7654  nqnq0a  7657  nqnq0m  7658  nq0m0r  7659  distrnq0  7662  mulcomnq0  7663  genipv  7712  genplt2i  7713  genpelvl  7715  genpelvu  7716  addnqprlemrl  7760  addnqprlemru  7761  addnqprlemfl  7762  addnqprlemfu  7763  addnqpr  7764  mulnqprlemrl  7776  mulnqprlemru  7777  mulnqprlemfl  7778  mulnqprlemfu  7779  mulnqpr  7780  distrlem4prl  7787  distrlem4pru  7788  ltnqpr  7796  recexprlemloc  7834  archrecnq  7866  mulclsr  7957  1idsr  7971  00sr  7972  prsradd  7989  axmulass  8076  axdistr  8077  axcnre  8084  peano5nnnn  8095  mulrid  8159  axltadd  8232  lenlt  8238  cnegexlem3  8339  cnegex  8340  resubcl  8426  subeqrev  8538  muladd  8546  mulsub  8563  mulsub2  8564  ltaddsub2  8600  leaddsub2  8602  leltadd  8610  ltaddpos2  8616  posdif  8618  addge02  8636  mullt0  8643  recexre  8741  recextlem1  8814  recexap  8816  divmuldivap  8875  conjmulap  8892  div2subap  9000  prodgt02  9016  prodge02  9018  lemul2  9020  lemul2a  9022  ltmulgt12  9028  lemulge12  9030  ltmuldiv2  9038  ltdivmul2  9041  ledivmul2  9043  lemuldiv2  9045  negiso  9118  cju  9124  peano5nni  9129  nnaddcl  9146  nnmulcl  9147  nnsub  9165  addltmul  9364  avgle1  9368  avgle2  9369  nnrecl  9383  nn0nnaddcl  9416  zsubcl  9503  zleloe  9509  znnsub  9514  nzadd  9515  zmulcl  9516  zltp1le  9517  zleltp1  9518  nnleltp1  9522  nnltp1le  9523  nnaddm1cl  9524  nn0ltp1le  9525  nn0leltp1  9526  nn0ltlem1  9527  znn0sub  9528  nn0sub  9529  elz2  9534  zapne  9537  zdcle  9539  zdclt  9540  zltlen  9541  nn0lem1lt  9546  nnlem1lt  9547  nnltlem1  9548  zdiv  9551  zextle  9554  zextlt  9555  btwnnz  9557  prime  9562  nneo  9566  peano2uz2  9570  peano5uzti  9571  uzind  9574  fzind  9578  fnn0ind  9579  uzneg  9758  uz11  9762  eluzp1m1  9763  eluzp1p1  9765  uzin  9772  indstr  9805  uz2mulcl  9820  qre  9837  qaddcl  9847  qsubcl  9850  qltlen  9852  qlttri2  9853  irradd  9858  elpqb  9862  cnref1o  9863  rpaddcl  9890  rpmulcl  9891  rpdivcl  9892  rexadd  10065  rexsub  10066  xaddcom  10074  xnn0xadd0  10080  xnegdi  10081  elicc2  10151  iccshftr  10207  iccshftl  10209  iccdil  10211  icccntr  10213  fzval2  10224  elfz1eq  10248  peano2fzr  10250  fznlem  10254  fzsplit2  10263  fzaddel  10272  fzsubel  10273  fzrev2  10298  fzrev3  10300  uzsplit  10305  fzrevral  10318  fzrevral3  10320  fzshftral  10321  elfz2nn0  10325  fznn0sub2  10341  fz0fzdiffz0  10343  elfzmlbp  10345  difelfzle  10347  difelfznle  10348  1fv  10352  elfzouz2  10375  fzo0n  10381  fzouzsplit  10394  fzoun  10396  elfzo0le  10402  fzonmapblen  10404  fzofzim  10405  fzoaddel2  10413  eluzgtdifelfzo  10420  elfzodifsumelfzo  10424  ubmelm1fzo  10449  fzofzp1b  10451  fzosplitprm1  10457  fzostep1  10460  subfzo0  10465  zsupcllemstep  10466  qdclt  10482  qbtwnxr  10494  flqbi2  10528  divfl0  10533  flqzadd  10535  flqmulnn0  10536  addmodidr  10612  modfzo0difsn  10634  frec2uzltd  10642  frec2uzrand  10644  frecfzen2  10666  seqshft2g  10721  seq3split  10727  seqsplitg  10728  seq3caopr2  10732  seqcaopr2g  10733  seqf1oglem2  10759  exp3vallem  10779  expcllem  10789  expcl2lemap  10790  1exp  10807  expge1  10815  expadd  10820  expmul  10823  expsubap  10826  leexp1a  10833  lt2sq  10852  le2sq  10853  sumsqeq0  10857  qsqeqor  10889  bernneq  10899  bernneq2  10900  sq11ap  10946  facdiv  10977  faclbnd  10980  faclbnd3  10982  faclbnd6  10983  facavg  10985  bcrpcl  10992  bccmpl  10993  fiubm  11068  seq3coll  11082  eqwrd  11130  ccatcl  11146  ccatclab  11147  ccatlen  11148  ccat0  11149  ccatval1  11150  ccatval2  11151  elfzelfzccat  11153  ccatvalfn  11154  ccatsymb  11155  ccatval21sw  11158  ccatrn  11162  lswccatn0lsw  11164  ccatalpha  11166  ccatrcl1  11167  swrdfv2  11216  swrdsbslen  11219  swrdspsleq  11220  swrdccat2  11224  pfxclz  11232  ccatpfx  11254  pfxccat1  11255  swrdswrdlem  11257  pfxswrd  11259  pfxccatin12lem4  11279  pfxccatin12lem1  11281  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccat3  11287  swrdccat  11288  pfxccatpfx2  11290  pfxccat3a  11291  swrdccat3blem  11292  swrdccat3b  11293  s2dmg  11343  shftfvalg  11350  shftf  11362  crre  11389  crim  11390  mulreap  11396  readd  11401  resub  11402  remul2  11405  imadd  11409  imsub  11410  immul2  11412  ipcnval  11418  cjsub  11424  cjreim  11435  caucvgre  11513  rexanuz  11520  rexuz3  11522  resqrexlemover  11542  resqrexlemcvg  11551  resqrexlemglsq  11554  sqrtle  11568  sqrtlt  11569  sqrt11ap  11570  sqrt11  11571  absreimsq  11599  absreim  11600  absmul  11601  sqabs  11614  absdiflt  11624  absdifle  11625  abssuble0  11635  abs2difabs  11640  fzomaxdif  11645  caubnd2  11649  rpmaxcl  11755  zmaxcl  11756  nn0maxcl  11757  minmax  11762  mincl  11763  min1inf  11764  min2inf  11765  minabs  11768  minclpr  11769  rpmincl  11770  2zinfmin  11775  xrmaxrecl  11787  xrminmax  11797  xrmincl  11798  xrmin1inf  11799  xrmin2inf  11800  xrminrecl  11805  xrminrpcl  11806  iooinsup  11809  climconst2  11823  climuni  11825  2clim  11833  climshft  11836  climshft2  11838  cjcn2  11848  climaddc1  11861  climmulc2  11863  climsubc1  11864  climsubc2  11865  climlec2  11873  summodclem2a  11913  zsumdc  11916  isumclim3  11955  mptfzshft  11974  fsumrev  11975  fisum0diag2  11979  telfsumo2  11999  fsumparts  12002  cvgcmpub  12008  binomlem  12015  binom1p  12017  binom1dif  12019  bcxmas  12021  isumshft  12022  expcnvap0  12034  expcnv  12036  geosergap  12038  geolim  12043  cvgratnnlemrate  12062  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  prodmodc  12110  zproddc  12111  fprodf1o  12120  fprodeq0  12149  efcj  12205  eftlub  12222  effsumlt  12224  efieq  12267  sinsub  12272  cossub  12273  subsin  12275  sinmul  12276  cosmul  12277  addcos  12278  subcos  12279  dvdssub2  12367  dvdsadd  12368  dvdsaddr  12369  dvdssub  12370  dvdssubr  12371  fzocongeq  12390  odd2np1  12405  opoe  12427  omoe  12428  opeo  12429  omeo  12430  divalgb  12457  ndvdsadd  12463  bitsfi  12489  gcdmndc  12497  gcdabs  12530  dvdsgcd  12554  absmulgcd  12559  gcdmultiple  12562  gcdmultiplez  12563  rpmulgcd  12568  sqgcd  12571  dvdssqlem  12572  dvdssq  12573  nninfctlemfo  12582  nn0seqcvgd  12584  ialgrlemconst  12586  algrf  12588  algrp1  12589  algcvg  12591  algcvga  12594  lcmval  12606  lcmabs  12619  lcmgcd  12621  lcmdvds  12622  lcmgcdnn  12625  coprmgcdb  12631  coprmdvds  12635  coprmdvds2  12636  qredeq  12639  isprm3  12661  nprm  12666  divgcdodd  12686  prmdvdsexp  12691  sqrt2irr  12705  zgcdsq  12744  hashdvds  12764  phiprmpw  12765  crth  12767  phimullem  12768  modprm0  12798  coprimeprodsq  12801  coprimeprodsq2  12802  pythagtriplem2  12810  pythagtriplem19  12826  pcdvdsb  12864  pcneg  12869  pc2dvds  12874  pc11  12875  pcmpt  12887  pcfac  12894  infpnlem1  12903  prmunb  12906  1arithlem4  12910  1arith  12911  gzaddcl  12921  gzmulcl  12922  gzreim  12923  gzsubcl  12924  4sqlem1  12932  4sqlem4a  12935  4sqlem4  12936  4sqlem12  12946  setsvalg  13083  setsfun0  13089  restval  13299  xpsval  13406  mndinvmod  13499  resmhm  13541  resmhm2  13542  mhmco  13544  dfgrp3m  13653  mhmmnd  13674  mulgnngsum  13685  mulgnn0z  13707  mulgnndir  13709  ghmex  13813  0ghm  13816  resghm  13818  resghm2  13819  ghmco  13822  ghmeql  13825  kerf1ghm  13832  ablsubsub23  13883  dfrhm2  14139  isrhm  14143  rhmfn  14157  rhmval  14158  rhmco  14159  resrhm  14233  rhmeql  14235  rhmima  14236  lmodfopne  14311  lspf  14374  znidom  14642  znrrg  14645  innei  14858  cnovex  14891  txuni2  14951  txbasex  14952  txbas  14953  txtop  14955  txtopon  14957  txss12  14961  txbasval  14962  txcnp  14966  upxp  14967  txcnmpt  14968  uptx  14969  txcn  14970  txrest  14971  txdis  14972  cnmpt21  14986  hmeoco  15011  txhmeo  15014  isxmet2d  15043  blin2  15127  comet  15194  metcn  15209  txmetcn  15214  qtopbasss  15216  qtopbas  15217  remetdval  15242  bl2ioo  15245  blssioo  15248  divcnap  15260  cncfmet  15287  dvaddxxbr  15396  dvcjbr  15403  plyf  15432  ply1termlem  15437  plymullem1  15443  plyaddlem  15444  plymullem  15445  plycolemc  15453  plyreres  15459  dvply1  15460  efle  15471  reapef  15473  sinperlem  15503  sincosq2sgn  15522  sincosq3sgn  15523  sincos6thpi  15537  ioocosf1o  15549  relogoprlem  15563  logleb  15570  cxple3  15616  cxpcom  15633  dvdsppwf1o  15684  fsumdvdsmul  15686  1sgmprm  15689  mersenne  15692  lgslem3  15702  lgsdir2  15733  lgsdir  15735  lgsdilem2  15736  lgsdi  15737  gausslemma2dlem1a  15758  gausslemma2dlem3  15763  gausslemma2dlem6  15767  lgseisenlem3  15772  lgseisenlem4  15773  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2  15783  lgsquad3  15784  2lgslem1a1  15786  2lgslem1a  15788  2lgslem1c  15790  2sqlem2  15815  mul2sq  15816  2sqlem7  15821  usgredg2v  16043  ushgredgedg  16045  ushgredgedgloop  16047  vtxedgfi  16075  vtxlpfi  16076  wlkeq  16126  uspgr2wlkeq  16137  clwwlkccatlem  16169  clwwlkccat  16170  clwwlknccat  16191  bj-inex  16379  bj-bdfindis  16419  triap  16511  cvgcmp2nlemabs  16514  trilpolemisumle  16520  inffz  16554