Theorem adantlr 477

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantlr	⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 283	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:  ad2antrr  488  ad2ant2r  509  ad2ant2rl  511  adantl3r  512  ad4ant14  514  ad4ant24  516  ad5ant13  519  ad5ant14  520  ad5ant15  521  3ad2antl1  1161  3ad2antl2  1162  ad4ant124  1218  3adant1r  1233  ad5ant235  1240  ad5ant135  1245  bilukdc  1407  intab  3900  pofun  4344  ralxfrd  4494  rexxfrd  4495  ordtri2or2exmidlem  4559  wessep  4611  poinxp  4729  relop  4813  fun11iun  5522  ssimaex  5619  fndmdif  5664  fconst2g  5774  foeqcnvco  5834  f1eqcocnv  5835  isocnv  5855  isocnv2  5856  riota2df  5895  caofdig  6161  f1o2ndf1  6283  tfr1onlembacc  6397  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllembacc  6410  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  tfrcl  6419  xpdom2  6887  fimax2gtrilemstep  6958  xpfi  6988  eqsupti  7057  ordiso2  7096  enumctlemm  7175  enwomnilem  7230  cc2lem  7328  mulcanpig  7397  prarloclemlt  7555  genpdf  7570  genpdisj  7585  addnqprl  7591  addnqpru  7592  addlocpr  7598  prmuloc  7628  mulnqprl  7630  mulnqpru  7631  mullocpr  7633  ltpopr  7657  ltsopr  7658  ltaddpr  7659  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  ltaprg  7681  recexprlemopu  7689  recexprlemloc  7693  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  suplocsrlem  7870  axcaucvglemcau  7960  axpre-suploclemres  7963  axsuploc  8094  cnegexlem1  8196  cnegexlem3  8198  cnegex  8199  addsubeq4  8236  rimul  8606  divcanap6  8740  ltmul12a  8881  lemul12b  8882  lbinf  8969  zrevaddcl  9370  nzadd  9372  zextle  9411  fzind  9435  uz11  9618  infregelbex  9666  qreccl  9710  qrevaddcl  9712  irradd  9714  xrlttr  9864  xrltso  9865  xaddass  9938  xleadd1a  9942  xlt2add  9949  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  divelunit  10071  uzsubsubfz  10116  fzaddel  10128  fzrev  10153  elfzmlbp  10201  frec2uzrdg  10483  frecuzrdgtcl  10486  frecuzrdgsuc  10488  frecuzrdgdomlem  10491  frecuzrdgfunlem  10493  frecuzrdgsuctlem  10497  iseqovex  10532  seq3val  10534  seqf  10538  seq3clss  10545  seq3fveq2  10549  seq3feq2  10550  seq3feq  10554  seq3shft2  10555  ser3mono  10561  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seq3caopr2  10567  seqcaopr2g  10568  iseqf1olemab  10576  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1oleml  10590  seqf1oglem2a  10592  seqf1oglem2  10594  seq3id3  10598  seq3id  10599  seq3id2  10600  seq3homo  10601  seq3z  10602  seqfeq3  10603  seqhomog  10604  seqfeq4g  10605  ser3ge0  10610  expp1  10620  expnegap0  10621  expcllem  10624  mulexp  10652  expadd  10655  expaddzap  10657  expmulzap  10659  expdivap  10664  leexp1a  10668  expnlbnd  10738  bcpasc  10840  bccl  10841  hashfacen  10910  seq3coll  10916  seq3shft  10985  resqrexlemfp1  11156  sqrtdiv  11189  climshftlemg  11448  climcn1  11454  climsqz  11481  climsqz2  11482  clim2ser  11483  clim2ser2  11484  isermulc2  11486  climub  11490  serf0  11498  fsum3cvg  11524  sumrbdc  11525  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsumf1o  11536  isumss  11537  fisumss  11538  isumss2  11539  fsum3cvg2  11540  fsum3cvg3  11542  fsumcl2lem  11544  fsumcllem  11545  fsumadd  11552  fsumsplit  11553  fsumsplitsn  11556  sumsplitdc  11578  fisumrev2  11592  fsum2mul  11599  fsum00  11608  telfsumo  11612  fsumparts  11616  iserabs  11621  cvgratnnlemabsle  11673  cvgratnn  11677  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  clim2prod  11685  clim2divap  11686  prodfap0  11691  prodfrecap  11692  prodeq2  11703  fproddccvg  11718  prodrbdclem2  11719  prodmodc  11724  zproddc  11725  fprodf1o  11734  fprodssdc  11736  fprodunsn  11750  fprodcllem  11752  fprodabs  11762  fprodeq0  11763  fprodmodd  11787  eftlcvg  11833  negdvdsb  11953  dvdsnegb  11954  dvdsext  12000  addmodlteqALT  12004  nno  12050  infssuzex  12089  zsupssdc  12094  gcdsupex  12097  gcdsupcl  12098  bezoutlembz  12144  dvdssq  12171  eucalgf  12196  dvdslcm  12210  lcmledvds  12211  lcmeq0  12212  lcmcl  12213  lcmdvds  12220  lcmgcdeq  12224  divgcdcoprmex  12243  isprm5lem  12282  phibndlem  12357  phiprmpw  12363  pc2dvds  12471  pcmpt  12484  prmpwdvds  12496  1arith  12508  4sqleminfi  12538  ctiunctlemf  12598  ctiunct  12600  grpinva  12972  grprida  12973  gsumpropd2  12979  sgrppropd  12999  mndpropd  13024  mhmpropd  13041  0mhm  13061  resmhm2  13063  resmhm2b  13064  grplcan  13137  mulgval  13195  mulgnn0z  13222  mulgnndir  13224  mulgnn0dir  13225  issubg2m  13262  issubg4m  13266  subgintm  13271  ghmf1  13346  gsumfzmptfidmadd  13412  gsumfzmhm  13416  srglmhm  13492  srgrmhm  13493  ringpropd  13537  crngpropd  13538  ringlghm  13560  ringrghm  13561  mulgass3  13584  issubrng2  13709  subrngpropd  13715  issubrg2  13740  subrgintm  13742  subrgpropd  13752  rhmpropd  13753  unitrrg  13766  lmodprop2d  13847  islss3  13878  lssintclm  13883  qusrhm  14027  gsumfzfsum  14087  opnssneib  14335  neissex  14344  tgrest  14348  iscnp3  14382  cnpnei  14398  cnrest  14414  tx1cn  14448  txcnp  14450  elbl3ps  14573  elbl3  14574  blininf  14603  blssexps  14608  blssex  14609  blpnfctr  14618  mopni2  14662  blsscls2  14672  metss  14673  bdmet  14681  metrest  14685  metcn  14693  txmetcn  14698  bl2ioo  14729  ivthinclemlr  14816  ivthinclemur  14818  dvcj  14888  dvfre  14889  elplyd  14920  plyaddlem1  14926  plymullem1  14927  plymullem  14929  plycolemc  14936  plycjlemc  14938  coseq0q4123  15010  abssinper  15022  lgsval2lem  15167  lgsval4lem  15168  lgsneg  15181  lgsmod  15183  lgsdir2  15190  lgsdir  15192  lgsne0  15195  lgssq  15197  lgsquadlem1  15234  subctctexmid  15561  cvgcmp2n  15593  iswomninnlem  15609  nconstwlpo  15626