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  3080  sylan9ss  3168  ssconb  3268  ineqan12d  3338  dfopg  3775  breqan12d  4017  opexg  4226  copsex2g  4244  ordin  4383  onin  4384  unexg  4441  eusv1  4450  opelvvg  4673  opthprc  4675  opbrop  4703  relop  4774  dmpropg  5098  unixpm  5161  funssres  5255  funinsn  5262  funtp  5266  fnco  5321  resasplitss  5392  fodmrnu  5443  relrnfvex  5530  fconst2g  5728  oveqan12d  5889  ovi3  6006  ovg  6008  f1opw2  6072  off  6090  offres  6131  iunon  6280  nnsucsssuc  6488  nnaword1  6509  ertr  6545  erex  6554  brecop  6620  ecovdi  6641  ecovidi  6642  mapvalg  6653  pmvalg  6654  pmss12g  6670  mapsn  6685  en2sn  6808  xpf1o  6839  xpen  6840  phplem4  6850  ssfilem  6870  diffitest  6882  en1eqsn  6942  sbthlem7  6957  ordiso  7030  updjud  7076  fodju0  7140  finnum  7177  pr2nelem  7185  djucomen  7210  exmidontriimlem1  7215  2onetap  7249  ltsopi  7314  pitric  7315  pitri3or  7316  ltdcpi  7317  mulclpi  7322  addcompig  7323  mulcompig  7325  distrpig  7327  ltexpi  7331  ltapig  7332  ltmpig  7333  dfplpq2  7348  dfmpq2  7349  enqbreq2  7351  enqdc  7355  addcmpblnq  7361  addpipqqslem  7363  mulpipq2  7365  mulpipq  7366  mulpipqqs  7367  addclnq  7369  distrnqg  7381  ltdcnq  7391  ltrnqg  7414  enq0breq  7430  addclnq0  7445  nqnq0a  7448  nqnq0m  7449  nq0m0r  7450  distrnq0  7453  mulcomnq0  7454  genipv  7503  genplt2i  7504  genpelvl  7506  genpelvu  7507  addnqprlemrl  7551  addnqprlemru  7552  addnqprlemfl  7553  addnqprlemfu  7554  addnqpr  7555  mulnqprlemrl  7567  mulnqprlemru  7568  mulnqprlemfl  7569  mulnqprlemfu  7570  mulnqpr  7571  distrlem4prl  7578  distrlem4pru  7579  ltnqpr  7587  recexprlemloc  7625  archrecnq  7657  mulclsr  7748  1idsr  7762  00sr  7763  prsradd  7780  axmulass  7867  axdistr  7868  axcnre  7875  peano5nnnn  7886  mulrid  7949  axltadd  8021  lenlt  8027  cnegexlem3  8128  cnegex  8129  resubcl  8215  subeqrev  8327  muladd  8335  mulsub  8352  mulsub2  8353  ltaddsub2  8388  leaddsub2  8390  leltadd  8398  ltaddpos2  8404  posdif  8406  addge02  8424  mullt0  8431  recexre  8529  recextlem1  8602  recexap  8604  divmuldivap  8663  conjmulap  8680  div2subap  8788  prodgt02  8804  prodge02  8806  lemul2  8808  lemul2a  8810  ltmulgt12  8816  lemulge12  8818  ltmuldiv2  8826  ltdivmul2  8829  ledivmul2  8831  lemuldiv2  8833  negiso  8906  cju  8912  peano5nni  8916  nnaddcl  8933  nnmulcl  8934  nnsub  8952  addltmul  9149  avgle1  9153  avgle2  9154  nnrecl  9168  nn0nnaddcl  9201  zsubcl  9288  zleloe  9294  znnsub  9298  nzadd  9299  zmulcl  9300  zltp1le  9301  zleltp1  9302  nnleltp1  9306  nnltp1le  9307  nnaddm1cl  9308  nn0ltp1le  9309  nn0leltp1  9310  nn0ltlem1  9311  znn0sub  9312  nn0sub  9313  elz2  9318  zapne  9321  zdcle  9323  zdclt  9324  zltlen  9325  nn0lem1lt  9330  nnlem1lt  9331  nnltlem1  9332  zdiv  9335  zextle  9338  zextlt  9339  btwnnz  9341  prime  9346  nneo  9350  peano2uz2  9354  peano5uzti  9355  uzind  9358  fzind  9362  fnn0ind  9363  uzneg  9540  uz11  9544  eluzp1m1  9545  eluzp1p1  9547  uzin  9554  indstr  9587  uz2mulcl  9602  qre  9619  qaddcl  9629  qsubcl  9632  qltlen  9634  qlttri2  9635  irradd  9640  elpqb  9643  cnref1o  9644  rpaddcl  9671  rpmulcl  9672  rpdivcl  9673  rexadd  9846  rexsub  9847  xaddcom  9855  xnn0xadd0  9861  xnegdi  9862  elicc2  9932  iccshftr  9988  iccshftl  9990  iccdil  9992  icccntr  9994  fzval2  10005  elfz1eq  10028  peano2fzr  10030  fznlem  10034  fzsplit2  10043  fzaddel  10052  fzsubel  10053  fzrev2  10078  fzrev3  10080  uzsplit  10085  fzrevral  10098  fzrevral3  10100  fzshftral  10101  elfz2nn0  10105  fznn0sub2  10121  fz0fzdiffz0  10123  elfzmlbp  10125  difelfzle  10127  difelfznle  10128  1fv  10132  elfzouz2  10154  fzouzsplit  10172  elfzo0le  10178  fzonmapblen  10180  fzofzim  10181  fzoaddel2  10186  eluzgtdifelfzo  10190  elfzodifsumelfzo  10194  ubmelm1fzo  10219  fzofzp1b  10221  fzosplitprm1  10227  fzostep1  10230  subfzo0  10235  qbtwnxr  10251  flqbi2  10284  divfl0  10289  flqzadd  10291  flqmulnn0  10292  addmodidr  10366  modfzo0difsn  10388  frec2uzltd  10396  frec2uzrand  10398  frecfzen2  10420  seq3split  10472  seq3caopr2  10475  exp3vallem  10514  expcllem  10524  expcl2lemap  10525  1exp  10542  expge1  10550  expadd  10555  expmul  10558  expsubap  10561  leexp1a  10568  lt2sq  10586  le2sq  10587  sumsqeq0  10591  qsqeqor  10623  bernneq  10633  bernneq2  10634  sq11ap  10680  facdiv  10709  faclbnd  10712  faclbnd3  10714  faclbnd6  10715  facavg  10717  bcrpcl  10724  bccmpl  10725  fiubm  10799  seq3coll  10813  shftfvalg  10818  shftf  10830  crre  10857  crim  10858  mulreap  10864  readd  10869  resub  10870  remul2  10873  imadd  10877  imsub  10878  immul2  10880  ipcnval  10886  cjsub  10892  cjreim  10903  caucvgre  10981  rexanuz  10988  rexuz3  10990  resqrexlemover  11010  resqrexlemcvg  11019  resqrexlemglsq  11022  sqrtle  11036  sqrtlt  11037  sqrt11ap  11038  sqrt11  11039  absreimsq  11067  absreim  11068  absmul  11069  sqabs  11082  absdiflt  11092  absdifle  11093  abssuble0  11103  abs2difabs  11108  fzomaxdif  11113  caubnd2  11117  rpmaxcl  11223  zmaxcl  11224  minmax  11229  mincl  11230  min1inf  11231  min2inf  11232  minabs  11235  minclpr  11236  rpmincl  11237  2zinfmin  11242  xrmaxrecl  11254  xrminmax  11264  xrmincl  11265  xrmin1inf  11266  xrmin2inf  11267  xrminrecl  11272  xrminrpcl  11273  iooinsup  11276  climconst2  11290  climuni  11292  2clim  11300  climshft  11303  climshft2  11305  cjcn2  11315  climaddc1  11328  climmulc2  11330  climsubc1  11331  climsubc2  11332  climlec2  11340  summodclem2a  11380  zsumdc  11383  isumclim3  11422  mptfzshft  11441  fsumrev  11442  fisum0diag2  11446  telfsumo2  11466  fsumparts  11469  cvgcmpub  11475  binomlem  11482  binom1p  11484  binom1dif  11486  bcxmas  11488  isumshft  11489  expcnvap0  11501  expcnv  11503  geosergap  11505  geolim  11510  cvgratnnlemrate  11529  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  prodmodc  11577  zproddc  11578  fprodf1o  11587  fprodeq0  11616  efcj  11672  eftlub  11689  effsumlt  11691  efieq  11734  sinsub  11739  cossub  11740  subsin  11742  sinmul  11743  cosmul  11744  addcos  11745  subcos  11746  dvdssub2  11833  dvdsadd  11834  dvdsaddr  11835  dvdssub  11836  dvdssubr  11837  fzocongeq  11854  odd2np1  11868  opoe  11890  omoe  11891  opeo  11892  omeo  11893  divalgb  11920  ndvdsadd  11926  zsupcllemstep  11936  gcdabs  11979  dvdsgcd  12003  absmulgcd  12008  gcdmultiple  12011  gcdmultiplez  12012  rpmulgcd  12017  sqgcd  12020  dvdssqlem  12021  dvdssq  12022  nn0seqcvgd  12031  ialgrlemconst  12033  algrf  12035  algrp1  12036  algcvg  12038  algcvga  12041  lcmval  12053  lcmabs  12066  lcmgcd  12068  lcmdvds  12069  lcmgcdnn  12072  coprmgcdb  12078  coprmdvds  12082  coprmdvds2  12083  qredeq  12086  isprm3  12108  nprm  12113  divgcdodd  12133  prmdvdsexp  12138  sqrt2irr  12152  zgcdsq  12191  hashdvds  12211  phiprmpw  12212  crth  12214  phimullem  12215  modprm0  12244  coprimeprodsq  12247  coprimeprodsq2  12248  pythagtriplem2  12256  pythagtriplem19  12272  pcdvdsb  12309  pcneg  12314  pc2dvds  12319  pc11  12320  pcmpt  12331  pcfac  12338  infpnlem1  12347  prmunb  12350  1arithlem4  12354  1arith  12355  gzaddcl  12365  gzmulcl  12366  gzreim  12367  gzsubcl  12368  4sqlem1  12376  4sqlem4a  12379  4sqlem4  12380  setsvalg  12482  setsfun0  12488  restval  12680  mndinvmod  12774  mhmco  12802  dfgrp3m  12897  mhmmnd  12908  mulgnn0z  12937  mulgnndir  12939  ablsubsub23  13028  innei  13445  cnovex  13478  txuni2  13538  txbasex  13539  txbas  13540  txtop  13542  txtopon  13544  txss12  13548  txbasval  13549  txcnp  13553  upxp  13554  txcnmpt  13555  uptx  13556  txcn  13557  txrest  13558  txdis  13559  cnmpt21  13573  hmeoco  13598  txhmeo  13601  isxmet2d  13630  blin2  13714  comet  13781  metcn  13796  txmetcn  13801  qtopbasss  13803  qtopbas  13804  remetdval  13821  bl2ioo  13824  blssioo  13827  divcnap  13837  cncfmet  13861  dvaddxxbr  13947  dvcjbr  13954  efle  13979  reapef  13981  sinperlem  14011  sincosq2sgn  14030  sincosq3sgn  14031  sincos6thpi  14045  ioocosf1o  14057  relogoprlem  14071  logleb  14078  cxple3  14123  cxpcom  14139  lgslem3  14185  lgsdir2  14216  lgsdir  14218  lgsdilem2  14219  lgsdi  14220  2sqlem2  14233  mul2sq  14234  2sqlem7  14239  bj-inex  14430  bj-bdfindis  14470  triap  14548  cvgcmp2nlemabs  14551  trilpolemisumle  14557  inffz  14590