Theorem syl2an 285

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 279	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2 282	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  syl2anr  286  anim12i  334  syl2an2  566  syl2an2r  567  mp3an3an  1302  eqeqan12d  2128  sylan9eq  2165  csbcomg  2990  sylan9ss  3074  ssconb  3173  ineqan12d  3243  dfopg  3667  breqan12d  3908  opexg  4108  copsex2g  4126  ordin  4265  onin  4266  unexg  4322  eusv1  4331  opelvvg  4546  opthprc  4548  opbrop  4576  relop  4647  dmpropg  4967  unixpm  5030  funssres  5121  funinsn  5128  funtp  5132  fnco  5187  resasplitss  5258  fodmrnu  5309  relrnfvex  5391  fconst2g  5587  oveqan12d  5745  ovi3  5859  ovg  5861  f1opw2  5928  off  5946  offres  5984  iunon  6132  nnsucsssuc  6339  nnaword1  6360  ertr  6395  erex  6404  brecop  6470  ecovdi  6491  ecovidi  6492  mapvalg  6503  pmvalg  6504  pmss12g  6520  mapsn  6535  en2sn  6658  xpf1o  6688  xpen  6689  phplem4  6699  ssfilem  6719  diffitest  6731  en1eqsn  6785  sbthlem7  6800  ordiso  6870  updjud  6916  fodju0  6966  finnum  6985  pr2nelem  6993  djucomen  7016  ltsopi  7069  pitric  7070  pitri3or  7071  ltdcpi  7072  mulclpi  7077  addcompig  7078  mulcompig  7080  distrpig  7082  ltexpi  7086  ltapig  7087  ltmpig  7088  dfplpq2  7103  dfmpq2  7104  enqbreq2  7106  enqdc  7110  addcmpblnq  7116  addpipqqslem  7118  mulpipq2  7120  mulpipq  7121  mulpipqqs  7122  addclnq  7124  distrnqg  7136  ltdcnq  7146  ltrnqg  7169  enq0breq  7185  addclnq0  7200  nqnq0a  7203  nqnq0m  7204  nq0m0r  7205  distrnq0  7208  mulcomnq0  7209  genipv  7258  genplt2i  7259  genpelvl  7261  genpelvu  7262  addnqprlemrl  7306  addnqprlemru  7307  addnqprlemfl  7308  addnqprlemfu  7309  addnqpr  7310  mulnqprlemrl  7322  mulnqprlemru  7323  mulnqprlemfl  7324  mulnqprlemfu  7325  mulnqpr  7326  distrlem4prl  7333  distrlem4pru  7334  ltnqpr  7342  recexprlemloc  7380  archrecnq  7412  mulclsr  7490  1idsr  7504  00sr  7505  prsradd  7521  axmulass  7601  axdistr  7602  axcnre  7609  peano5nnnn  7620  mulid1  7680  axltadd  7751  lenlt  7756  cnegexlem3  7855  cnegex  7856  resubcl  7942  subeqrev  8050  muladd  8058  mulsub  8075  mulsub2  8076  ltaddsub2  8111  leaddsub2  8113  leltadd  8121  ltaddpos2  8127  posdif  8129  addge02  8147  mullt0  8154  recexre  8251  recextlem1  8318  recexap  8320  divmuldivap  8378  conjmulap  8395  div2subap  8502  prodgt02  8514  prodge02  8516  lemul2  8518  lemul2a  8520  ltmulgt12  8526  lemulge12  8528  ltmuldiv2  8536  ltdivmul2  8539  ledivmul2  8541  lemuldiv2  8543  negiso  8616  cju  8622  peano5nni  8626  nnaddcl  8643  nnmulcl  8644  nnsub  8662  addltmul  8853  avgle1  8857  avgle2  8858  nnrecl  8872  nn0nnaddcl  8905  zsubcl  8992  zleloe  8998  znnsub  9002  nzadd  9003  zmulcl  9004  zltp1le  9005  zleltp1  9006  nnleltp1  9010  nnltp1le  9011  nnaddm1cl  9012  nn0ltp1le  9013  nn0leltp1  9014  nn0ltlem1  9015  znn0sub  9016  nn0sub  9017  elz2  9019  zapne  9022  zdcle  9024  zdclt  9025  zltlen  9026  nn0lem1lt  9031  nnlem1lt  9032  nnltlem1  9033  zdiv  9036  zextle  9039  zextlt  9040  btwnnz  9042  prime  9047  nneo  9051  peano2uz2  9055  peano5uzti  9056  uzind  9059  fzind  9063  fnn0ind  9064  uzneg  9239  uz11  9243  eluzp1m1  9244  eluzp1p1  9246  uzin  9253  indstr  9283  uz2mulcl  9297  qre  9312  qaddcl  9322  qsubcl  9325  qltlen  9327  qlttri2  9328  irradd  9333  cnref1o  9335  rpaddcl  9359  rpmulcl  9360  rpdivcl  9361  rexadd  9521  rexsub  9522  xaddcom  9530  xnn0xadd0  9536  xnegdi  9537  elicc2  9607  iccshftr  9663  iccshftl  9665  iccdil  9667  icccntr  9669  fzval2  9679  elfz1eq  9701  peano2fzr  9703  fznlem  9707  fzsplit2  9716  fzaddel  9725  fzsubel  9726  fzrev2  9751  fzrev3  9753  uzsplit  9758  fzrevral  9771  fzrevral3  9773  fzshftral  9774  elfz2nn0  9778  fznn0sub2  9791  fz0fzdiffz0  9793  elfzmlbp  9795  difelfzle  9797  difelfznle  9798  1fv  9802  elfzouz2  9824  fzouzsplit  9842  elfzo0le  9848  fzonmapblen  9850  fzofzim  9851  fzoaddel2  9856  eluzgtdifelfzo  9860  elfzodifsumelfzo  9864  ubmelm1fzo  9889  fzofzp1b  9891  fzosplitprm1  9897  fzostep1  9900  subfzo0  9905  qbtwnxr  9921  flqbi2  9950  divfl0  9955  flqzadd  9957  flqmulnn0  9958  addmodidr  10032  modfzo0difsn  10054  frec2uzltd  10062  frec2uzrand  10064  frecfzen2  10086  seq3split  10138  seq3caopr2  10141  exp3vallem  10180  expcllem  10190  expcl2lemap  10191  1exp  10208  expge1  10216  expadd  10221  expmul  10224  expsubap  10227  leexp1a  10234  lt2sq  10252  le2sq  10253  sumsqeq0  10257  bernneq  10298  bernneq2  10299  sq11ap  10344  facdiv  10370  faclbnd  10373  faclbnd3  10375  faclbnd6  10376  facavg  10378  bcrpcl  10385  bccmpl  10386  seq3coll  10471  shftfvalg  10476  shftf  10488  crre  10515  crim  10516  mulreap  10522  readd  10527  resub  10528  remul2  10531  imadd  10535  imsub  10536  immul2  10538  ipcnval  10544  cjsub  10550  cjreim  10561  caucvgre  10638  rexanuz  10645  rexuz3  10647  resqrexlemover  10667  resqrexlemcvg  10676  resqrexlemglsq  10679  sqrtle  10693  sqrtlt  10694  sqrt11ap  10695  sqrt11  10696  absreimsq  10724  absreim  10725  absmul  10726  sqabs  10739  absdiflt  10749  absdifle  10750  abssuble0  10760  abs2difabs  10765  fzomaxdif  10770  caubnd2  10774  rpmaxcl  10880  zmaxcl  10881  minmax  10886  mincl  10887  min1inf  10888  min2inf  10889  minabs  10892  minclpr  10893  rpmincl  10894  xrmaxrecl  10909  xrminmax  10919  xrmincl  10920  xrmin1inf  10921  xrmin2inf  10922  xrminrecl  10927  xrminrpcl  10928  iooinsup  10931  climconst2  10945  climuni  10947  2clim  10955  climshft  10958  climshft2  10960  cjcn2  10970  climaddc1  10983  climmulc2  10985  climsubc1  10986  climsubc2  10987  climlec2  10995  summodclem2a  11035  zsumdc  11038  isumclim3  11077  mptfzshft  11096  fsumrev  11097  fisum0diag2  11101  telfsumo2  11121  fsumparts  11124  cvgcmpub  11130  binomlem  11137  binom1p  11139  binom1dif  11141  bcxmas  11143  isumshft  11144  expcnvap0  11156  expcnv  11158  geosergap  11160  geolim  11165  cvgratnnlemrate  11184  mertenslemi1  11189  mertenslem2  11190  mertensabs  11191  efcj  11223  eftlub  11240  effsumlt  11242  efieq  11286  sinsub  11291  cossub  11292  subsin  11294  sinmul  11295  cosmul  11296  addcos  11297  subcos  11298  dvdssub2  11376  dvdsadd  11377  dvdsaddr  11378  dvdssub  11379  dvdssubr  11380  fzocongeq  11397  odd2np1  11411  opoe  11433  omoe  11434  opeo  11435  omeo  11436  divalgb  11463  ndvdsadd  11469  zsupcllemstep  11479  gcdabs  11517  dvdsgcd  11539  absmulgcd  11544  gcdmultiple  11547  gcdmultiplez  11548  rpmulgcd  11553  sqgcd  11556  dvdssqlem  11557  dvdssq  11558  nn0seqcvgd  11561  ialgrlemconst  11563  algrf  11565  algrp1  11566  algcvg  11568  algcvga  11571  lcmval  11583  lcmabs  11596  lcmgcd  11598  lcmdvds  11599  lcmgcdnn  11602  coprmgcdb  11608  coprmdvds  11612  coprmdvds2  11613  qredeq  11616  isprm3  11638  nprm  11643  divgcdodd  11660  prmdvdsexp  11665  sqrt2irr  11679  zgcdsq  11717  hashdvds  11735  phiprmpw  11736  crth  11738  phimullem  11739  setsvalg  11825  setsfun0  11831  restval  11962  innei  12168  txuni2  12260  txbasex  12261  txbas  12262  txtop  12264  txtopon  12266  txss12  12270  txbasval  12271  txcnp  12275  upxp  12276  txcnmpt  12277  uptx  12278  txcn  12279  txrest  12280  txdis  12281  cnmpt21  12295  isxmet2d  12330  blin2  12414  comet  12481  metcn  12496  txmetcn  12501  qtopbasss  12503  qtopbas  12504  remetdval  12518  bl2ioo  12521  blssioo  12524  divcnap  12534  cncfmet  12558  bj-inex  12784  bj-bdfindis  12824  triap  12901  cvgcmp2nlemabs  12904  trilpolemisumle  12908  inffz  12915