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  3776  breqan12d  4019  opexg  4228  copsex2g  4246  ordin  4385  onin  4386  unexg  4443  eusv1  4452  opelvvg  4675  opthprc  4677  opbrop  4705  relop  4777  dmpropg  5101  unixpm  5164  funssres  5258  funinsn  5265  funtp  5269  fnco  5324  resasplitss  5395  fodmrnu  5446  relrnfvex  5533  fconst2g  5731  oveqan12d  5893  ovi3  6010  ovg  6012  f1opw2  6076  off  6094  offres  6135  iunon  6284  nnsucsssuc  6492  nnaword1  6513  ertr  6549  erex  6558  brecop  6624  ecovdi  6645  ecovidi  6646  mapvalg  6657  pmvalg  6658  pmss12g  6674  mapsn  6689  en2sn  6812  xpf1o  6843  xpen  6844  phplem4  6854  ssfilem  6874  diffitest  6886  en1eqsn  6946  sbthlem7  6961  ordiso  7034  updjud  7080  fodju0  7144  finnum  7181  pr2nelem  7189  djucomen  7214  exmidontriimlem1  7219  2onetap  7253  ltsopi  7318  pitric  7319  pitri3or  7320  ltdcpi  7321  mulclpi  7326  addcompig  7327  mulcompig  7329  distrpig  7331  ltexpi  7335  ltapig  7336  ltmpig  7337  dfplpq2  7352  dfmpq2  7353  enqbreq2  7355  enqdc  7359  addcmpblnq  7365  addpipqqslem  7367  mulpipq2  7369  mulpipq  7370  mulpipqqs  7371  addclnq  7373  distrnqg  7385  ltdcnq  7395  ltrnqg  7418  enq0breq  7434  addclnq0  7449  nqnq0a  7452  nqnq0m  7453  nq0m0r  7454  distrnq0  7457  mulcomnq0  7458  genipv  7507  genplt2i  7508  genpelvl  7510  genpelvu  7511  addnqprlemrl  7555  addnqprlemru  7556  addnqprlemfl  7557  addnqprlemfu  7558  addnqpr  7559  mulnqprlemrl  7571  mulnqprlemru  7572  mulnqprlemfl  7573  mulnqprlemfu  7574  mulnqpr  7575  distrlem4prl  7582  distrlem4pru  7583  ltnqpr  7591  recexprlemloc  7629  archrecnq  7661  mulclsr  7752  1idsr  7766  00sr  7767  prsradd  7784  axmulass  7871  axdistr  7872  axcnre  7879  peano5nnnn  7890  mulrid  7953  axltadd  8026  lenlt  8032  cnegexlem3  8133  cnegex  8134  resubcl  8220  subeqrev  8332  muladd  8340  mulsub  8357  mulsub2  8358  ltaddsub2  8393  leaddsub2  8395  leltadd  8403  ltaddpos2  8409  posdif  8411  addge02  8429  mullt0  8436  recexre  8534  recextlem1  8607  recexap  8609  divmuldivap  8668  conjmulap  8685  div2subap  8793  prodgt02  8809  prodge02  8811  lemul2  8813  lemul2a  8815  ltmulgt12  8821  lemulge12  8823  ltmuldiv2  8831  ltdivmul2  8834  ledivmul2  8836  lemuldiv2  8838  negiso  8911  cju  8917  peano5nni  8921  nnaddcl  8938  nnmulcl  8939  nnsub  8957  addltmul  9154  avgle1  9158  avgle2  9159  nnrecl  9173  nn0nnaddcl  9206  zsubcl  9293  zleloe  9299  znnsub  9303  nzadd  9304  zmulcl  9305  zltp1le  9306  zleltp1  9307  nnleltp1  9311  nnltp1le  9312  nnaddm1cl  9313  nn0ltp1le  9314  nn0leltp1  9315  nn0ltlem1  9316  znn0sub  9317  nn0sub  9318  elz2  9323  zapne  9326  zdcle  9328  zdclt  9329  zltlen  9330  nn0lem1lt  9335  nnlem1lt  9336  nnltlem1  9337  zdiv  9340  zextle  9343  zextlt  9344  btwnnz  9346  prime  9351  nneo  9355  peano2uz2  9359  peano5uzti  9360  uzind  9363  fzind  9367  fnn0ind  9368  uzneg  9545  uz11  9549  eluzp1m1  9550  eluzp1p1  9552  uzin  9559  indstr  9592  uz2mulcl  9607  qre  9624  qaddcl  9634  qsubcl  9637  qltlen  9639  qlttri2  9640  irradd  9645  elpqb  9648  cnref1o  9649  rpaddcl  9676  rpmulcl  9677  rpdivcl  9678  rexadd  9851  rexsub  9852  xaddcom  9860  xnn0xadd0  9866  xnegdi  9867  elicc2  9937  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  fzval2  10010  elfz1eq  10034  peano2fzr  10036  fznlem  10040  fzsplit2  10049  fzaddel  10058  fzsubel  10059  fzrev2  10084  fzrev3  10086  uzsplit  10091  fzrevral  10104  fzrevral3  10106  fzshftral  10107  elfz2nn0  10111  fznn0sub2  10127  fz0fzdiffz0  10129  elfzmlbp  10131  difelfzle  10133  difelfznle  10134  1fv  10138  elfzouz2  10160  fzouzsplit  10178  elfzo0le  10184  fzonmapblen  10186  fzofzim  10187  fzoaddel2  10192  eluzgtdifelfzo  10196  elfzodifsumelfzo  10200  ubmelm1fzo  10225  fzofzp1b  10227  fzosplitprm1  10233  fzostep1  10236  subfzo0  10241  qbtwnxr  10257  flqbi2  10290  divfl0  10295  flqzadd  10297  flqmulnn0  10298  addmodidr  10372  modfzo0difsn  10394  frec2uzltd  10402  frec2uzrand  10404  frecfzen2  10426  seq3split  10478  seq3caopr2  10481  exp3vallem  10520  expcllem  10530  expcl2lemap  10531  1exp  10548  expge1  10556  expadd  10561  expmul  10564  expsubap  10567  leexp1a  10574  lt2sq  10593  le2sq  10594  sumsqeq0  10598  qsqeqor  10630  bernneq  10640  bernneq2  10641  sq11ap  10687  facdiv  10717  faclbnd  10720  faclbnd3  10722  faclbnd6  10723  facavg  10725  bcrpcl  10732  bccmpl  10733  fiubm  10807  seq3coll  10821  shftfvalg  10826  shftf  10838  crre  10865  crim  10866  mulreap  10872  readd  10877  resub  10878  remul2  10881  imadd  10885  imsub  10886  immul2  10888  ipcnval  10894  cjsub  10900  cjreim  10911  caucvgre  10989  rexanuz  10996  rexuz3  10998  resqrexlemover  11018  resqrexlemcvg  11027  resqrexlemglsq  11030  sqrtle  11044  sqrtlt  11045  sqrt11ap  11046  sqrt11  11047  absreimsq  11075  absreim  11076  absmul  11077  sqabs  11090  absdiflt  11100  absdifle  11101  abssuble0  11111  abs2difabs  11116  fzomaxdif  11121  caubnd2  11125  rpmaxcl  11231  zmaxcl  11232  minmax  11237  mincl  11238  min1inf  11239  min2inf  11240  minabs  11243  minclpr  11244  rpmincl  11245  2zinfmin  11250  xrmaxrecl  11262  xrminmax  11272  xrmincl  11273  xrmin1inf  11274  xrmin2inf  11275  xrminrecl  11280  xrminrpcl  11281  iooinsup  11284  climconst2  11298  climuni  11300  2clim  11308  climshft  11311  climshft2  11313  cjcn2  11323  climaddc1  11336  climmulc2  11338  climsubc1  11339  climsubc2  11340  climlec2  11348  summodclem2a  11388  zsumdc  11391  isumclim3  11430  mptfzshft  11449  fsumrev  11450  fisum0diag2  11454  telfsumo2  11474  fsumparts  11477  cvgcmpub  11483  binomlem  11490  binom1p  11492  binom1dif  11494  bcxmas  11496  isumshft  11497  expcnvap0  11509  expcnv  11511  geosergap  11513  geolim  11518  cvgratnnlemrate  11537  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodmodc  11585  zproddc  11586  fprodf1o  11595  fprodeq0  11624  efcj  11680  eftlub  11697  effsumlt  11699  efieq  11742  sinsub  11747  cossub  11748  subsin  11750  sinmul  11751  cosmul  11752  addcos  11753  subcos  11754  dvdssub2  11841  dvdsadd  11842  dvdsaddr  11843  dvdssub  11844  dvdssubr  11845  fzocongeq  11863  odd2np1  11877  opoe  11899  omoe  11900  opeo  11901  omeo  11902  divalgb  11929  ndvdsadd  11935  zsupcllemstep  11945  gcdabs  11988  dvdsgcd  12012  absmulgcd  12017  gcdmultiple  12020  gcdmultiplez  12021  rpmulgcd  12026  sqgcd  12029  dvdssqlem  12030  dvdssq  12031  nn0seqcvgd  12040  ialgrlemconst  12042  algrf  12044  algrp1  12045  algcvg  12047  algcvga  12050  lcmval  12062  lcmabs  12075  lcmgcd  12077  lcmdvds  12078  lcmgcdnn  12081  coprmgcdb  12087  coprmdvds  12091  coprmdvds2  12092  qredeq  12095  isprm3  12117  nprm  12122  divgcdodd  12142  prmdvdsexp  12147  sqrt2irr  12161  zgcdsq  12200  hashdvds  12220  phiprmpw  12221  crth  12223  phimullem  12224  modprm0  12253  coprimeprodsq  12256  coprimeprodsq2  12257  pythagtriplem2  12265  pythagtriplem19  12281  pcdvdsb  12318  pcneg  12323  pc2dvds  12328  pc11  12329  pcmpt  12340  pcfac  12347  infpnlem1  12356  prmunb  12359  1arithlem4  12363  1arith  12364  gzaddcl  12374  gzmulcl  12375  gzreim  12376  gzsubcl  12377  4sqlem1  12385  4sqlem4a  12388  4sqlem4  12389  setsvalg  12491  setsfun0  12497  restval  12693  xpsval  12770  mndinvmod  12845  mhmco  12873  dfgrp3m  12968  mhmmnd  12979  mulgnn0z  13008  mulgnndir  13010  ablsubsub23  13126  innei  13633  cnovex  13666  txuni2  13726  txbasex  13727  txbas  13728  txtop  13730  txtopon  13732  txss12  13736  txbasval  13737  txcnp  13741  upxp  13742  txcnmpt  13743  uptx  13744  txcn  13745  txrest  13746  txdis  13747  cnmpt21  13761  hmeoco  13786  txhmeo  13789  isxmet2d  13818  blin2  13902  comet  13969  metcn  13984  txmetcn  13989  qtopbasss  13991  qtopbas  13992  remetdval  14009  bl2ioo  14012  blssioo  14015  divcnap  14025  cncfmet  14049  dvaddxxbr  14135  dvcjbr  14142  efle  14167  reapef  14169  sinperlem  14199  sincosq2sgn  14218  sincosq3sgn  14219  sincos6thpi  14233  ioocosf1o  14245  relogoprlem  14259  logleb  14266  cxple3  14311  cxpcom  14327  lgslem3  14373  lgsdir2  14404  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  2sqlem2  14432  mul2sq  14433  2sqlem7  14438  bj-inex  14629  bj-bdfindis  14669  triap  14747  cvgcmp2nlemabs  14750  trilpolemisumle  14756  inffz  14789