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  594  syl2an2r  595  mp3an3an  1343  eqeqan12d  2193  sylan9eq  2230  csbcomg  3081  sylan9ss  3169  ssconb  3269  ineqan12d  3339  dfopg  3777  breqan12d  4020  opexg  4229  copsex2g  4247  ordin  4386  onin  4387  unexg  4444  eusv1  4453  opelvvg  4676  opthprc  4678  opbrop  4706  relop  4778  dmpropg  5102  unixpm  5165  funssres  5259  funinsn  5266  funtp  5270  fnco  5325  resasplitss  5396  fodmrnu  5447  relrnfvex  5534  fconst2g  5732  oveqan12d  5894  ovi3  6011  ovg  6013  f1opw2  6077  off  6095  offres  6136  iunon  6285  nnsucsssuc  6493  nnaword1  6514  ertr  6550  erex  6559  brecop  6625  ecovdi  6646  ecovidi  6647  mapvalg  6658  pmvalg  6659  pmss12g  6675  mapsn  6690  en2sn  6813  xpf1o  6844  xpen  6845  phplem4  6855  ssfilem  6875  diffitest  6887  en1eqsn  6947  sbthlem7  6962  ordiso  7035  updjud  7081  fodju0  7145  finnum  7182  pr2nelem  7190  djucomen  7215  exmidontriimlem1  7220  2onetap  7254  ltsopi  7319  pitric  7320  pitri3or  7321  ltdcpi  7322  mulclpi  7327  addcompig  7328  mulcompig  7330  distrpig  7332  ltexpi  7336  ltapig  7337  ltmpig  7338  dfplpq2  7353  dfmpq2  7354  enqbreq2  7356  enqdc  7360  addcmpblnq  7366  addpipqqslem  7368  mulpipq2  7370  mulpipq  7371  mulpipqqs  7372  addclnq  7374  distrnqg  7386  ltdcnq  7396  ltrnqg  7419  enq0breq  7435  addclnq0  7450  nqnq0a  7453  nqnq0m  7454  nq0m0r  7455  distrnq0  7458  mulcomnq0  7459  genipv  7508  genplt2i  7509  genpelvl  7511  genpelvu  7512  addnqprlemrl  7556  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  addnqpr  7560  mulnqprlemrl  7572  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  mulnqpr  7576  distrlem4prl  7583  distrlem4pru  7584  ltnqpr  7592  recexprlemloc  7630  archrecnq  7662  mulclsr  7753  1idsr  7767  00sr  7768  prsradd  7785  axmulass  7872  axdistr  7873  axcnre  7880  peano5nnnn  7891  mulrid  7954  axltadd  8027  lenlt  8033  cnegexlem3  8134  cnegex  8135  resubcl  8221  subeqrev  8333  muladd  8341  mulsub  8358  mulsub2  8359  ltaddsub2  8394  leaddsub2  8396  leltadd  8404  ltaddpos2  8410  posdif  8412  addge02  8430  mullt0  8437  recexre  8535  recextlem1  8608  recexap  8610  divmuldivap  8669  conjmulap  8686  div2subap  8794  prodgt02  8810  prodge02  8812  lemul2  8814  lemul2a  8816  ltmulgt12  8822  lemulge12  8824  ltmuldiv2  8832  ltdivmul2  8835  ledivmul2  8837  lemuldiv2  8839  negiso  8912  cju  8918  peano5nni  8922  nnaddcl  8939  nnmulcl  8940  nnsub  8958  addltmul  9155  avgle1  9159  avgle2  9160  nnrecl  9174  nn0nnaddcl  9207  zsubcl  9294  zleloe  9300  znnsub  9304  nzadd  9305  zmulcl  9306  zltp1le  9307  zleltp1  9308  nnleltp1  9312  nnltp1le  9313  nnaddm1cl  9314  nn0ltp1le  9315  nn0leltp1  9316  nn0ltlem1  9317  znn0sub  9318  nn0sub  9319  elz2  9324  zapne  9327  zdcle  9329  zdclt  9330  zltlen  9331  nn0lem1lt  9336  nnlem1lt  9337  nnltlem1  9338  zdiv  9341  zextle  9344  zextlt  9345  btwnnz  9347  prime  9352  nneo  9356  peano2uz2  9360  peano5uzti  9361  uzind  9364  fzind  9368  fnn0ind  9369  uzneg  9546  uz11  9550  eluzp1m1  9551  eluzp1p1  9553  uzin  9560  indstr  9593  uz2mulcl  9608  qre  9625  qaddcl  9635  qsubcl  9638  qltlen  9640  qlttri2  9641  irradd  9646  elpqb  9649  cnref1o  9650  rpaddcl  9677  rpmulcl  9678  rpdivcl  9679  rexadd  9852  rexsub  9853  xaddcom  9861  xnn0xadd0  9867  xnegdi  9868  elicc2  9938  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  fzval2  10011  elfz1eq  10035  peano2fzr  10037  fznlem  10041  fzsplit2  10050  fzaddel  10059  fzsubel  10060  fzrev2  10085  fzrev3  10087  uzsplit  10092  fzrevral  10105  fzrevral3  10107  fzshftral  10108  elfz2nn0  10112  fznn0sub2  10128  fz0fzdiffz0  10130  elfzmlbp  10132  difelfzle  10134  difelfznle  10135  1fv  10139  elfzouz2  10161  fzouzsplit  10179  elfzo0le  10185  fzonmapblen  10187  fzofzim  10188  fzoaddel2  10193  eluzgtdifelfzo  10197  elfzodifsumelfzo  10201  ubmelm1fzo  10226  fzofzp1b  10228  fzosplitprm1  10234  fzostep1  10237  subfzo0  10242  qbtwnxr  10258  flqbi2  10291  divfl0  10296  flqzadd  10298  flqmulnn0  10299  addmodidr  10373  modfzo0difsn  10395  frec2uzltd  10403  frec2uzrand  10405  frecfzen2  10427  seq3split  10479  seq3caopr2  10482  exp3vallem  10521  expcllem  10531  expcl2lemap  10532  1exp  10549  expge1  10557  expadd  10562  expmul  10565  expsubap  10568  leexp1a  10575  lt2sq  10594  le2sq  10595  sumsqeq0  10599  qsqeqor  10631  bernneq  10641  bernneq2  10642  sq11ap  10688  facdiv  10718  faclbnd  10721  faclbnd3  10723  faclbnd6  10724  facavg  10726  bcrpcl  10733  bccmpl  10734  fiubm  10808  seq3coll  10822  shftfvalg  10827  shftf  10839  crre  10866  crim  10867  mulreap  10873  readd  10878  resub  10879  remul2  10882  imadd  10886  imsub  10887  immul2  10889  ipcnval  10895  cjsub  10901  cjreim  10912  caucvgre  10990  rexanuz  10997  rexuz3  10999  resqrexlemover  11019  resqrexlemcvg  11028  resqrexlemglsq  11031  sqrtle  11045  sqrtlt  11046  sqrt11ap  11047  sqrt11  11048  absreimsq  11076  absreim  11077  absmul  11078  sqabs  11091  absdiflt  11101  absdifle  11102  abssuble0  11112  abs2difabs  11117  fzomaxdif  11122  caubnd2  11126  rpmaxcl  11232  zmaxcl  11233  minmax  11238  mincl  11239  min1inf  11240  min2inf  11241  minabs  11244  minclpr  11245  rpmincl  11246  2zinfmin  11251  xrmaxrecl  11263  xrminmax  11273  xrmincl  11274  xrmin1inf  11275  xrmin2inf  11276  xrminrecl  11281  xrminrpcl  11282  iooinsup  11285  climconst2  11299  climuni  11301  2clim  11309  climshft  11312  climshft2  11314  cjcn2  11324  climaddc1  11337  climmulc2  11339  climsubc1  11340  climsubc2  11341  climlec2  11349  summodclem2a  11389  zsumdc  11392  isumclim3  11431  mptfzshft  11450  fsumrev  11451  fisum0diag2  11455  telfsumo2  11475  fsumparts  11478  cvgcmpub  11484  binomlem  11491  binom1p  11493  binom1dif  11495  bcxmas  11497  isumshft  11498  expcnvap0  11510  expcnv  11512  geosergap  11514  geolim  11519  cvgratnnlemrate  11538  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodmodc  11586  zproddc  11587  fprodf1o  11596  fprodeq0  11625  efcj  11681  eftlub  11698  effsumlt  11700  efieq  11743  sinsub  11748  cossub  11749  subsin  11751  sinmul  11752  cosmul  11753  addcos  11754  subcos  11755  dvdssub2  11842  dvdsadd  11843  dvdsaddr  11844  dvdssub  11845  dvdssubr  11846  fzocongeq  11864  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  divalgb  11930  ndvdsadd  11936  zsupcllemstep  11946  gcdabs  11989  dvdsgcd  12013  absmulgcd  12018  gcdmultiple  12021  gcdmultiplez  12022  rpmulgcd  12027  sqgcd  12030  dvdssqlem  12031  dvdssq  12032  nn0seqcvgd  12041  ialgrlemconst  12043  algrf  12045  algrp1  12046  algcvg  12048  algcvga  12051  lcmval  12063  lcmabs  12076  lcmgcd  12078  lcmdvds  12079  lcmgcdnn  12082  coprmgcdb  12088  coprmdvds  12092  coprmdvds2  12093  qredeq  12096  isprm3  12118  nprm  12123  divgcdodd  12143  prmdvdsexp  12148  sqrt2irr  12162  zgcdsq  12201  hashdvds  12221  phiprmpw  12222  crth  12224  phimullem  12225  modprm0  12254  coprimeprodsq  12257  coprimeprodsq2  12258  pythagtriplem2  12266  pythagtriplem19  12282  pcdvdsb  12319  pcneg  12324  pc2dvds  12329  pc11  12330  pcmpt  12341  pcfac  12348  infpnlem1  12357  prmunb  12360  1arithlem4  12364  1arith  12365  gzaddcl  12375  gzmulcl  12376  gzreim  12377  gzsubcl  12378  4sqlem1  12386  4sqlem4a  12389  4sqlem4  12390  setsvalg  12492  setsfun0  12498  restval  12694  xpsval  12771  mndinvmod  12846  mhmco  12874  dfgrp3m  12969  mhmmnd  12980  mulgnn0z  13010  mulgnndir  13012  ablsubsub23  13128  lmodfopne  13416  innei  13666  cnovex  13699  txuni2  13759  txbasex  13760  txbas  13761  txtop  13763  txtopon  13765  txss12  13769  txbasval  13770  txcnp  13774  upxp  13775  txcnmpt  13776  uptx  13777  txcn  13778  txrest  13779  txdis  13780  cnmpt21  13794  hmeoco  13819  txhmeo  13822  isxmet2d  13851  blin2  13935  comet  14002  metcn  14017  txmetcn  14022  qtopbasss  14024  qtopbas  14025  remetdval  14042  bl2ioo  14045  blssioo  14048  divcnap  14058  cncfmet  14082  dvaddxxbr  14168  dvcjbr  14175  efle  14200  reapef  14202  sinperlem  14232  sincosq2sgn  14251  sincosq3sgn  14252  sincos6thpi  14266  ioocosf1o  14278  relogoprlem  14292  logleb  14299  cxple3  14344  cxpcom  14360  lgslem3  14406  lgsdir2  14437  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  2sqlem2  14465  mul2sq  14466  2sqlem7  14471  bj-inex  14662  bj-bdfindis  14702  triap  14780  cvgcmp2nlemabs  14783  trilpolemisumle  14789  inffz  14822