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  1183  3ad2antl2  1184  ad4ant124  1240  3adant1r  1255  ad5ant235  1262  ad5ant135  1267  bilukdc  1438  elpr2elpr  3854  intab  3952  pofun  4403  ralxfrd  4553  rexxfrd  4554  ordtri2or2exmidlem  4618  wessep  4670  poinxp  4788  relop  4872  fun11iun  5595  ssimaex  5697  fndmdif  5742  fconst2g  5858  foeqcnvco  5920  f1eqcocnv  5921  isocnv  5941  isocnv2  5942  riota2df  5982  caofdig  6258  f1o2ndf1  6380  tfr1onlembacc  6494  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllembacc  6507  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  tfrcl  6516  xpdom2  6998  fimax2gtrilemstep  7070  xpfi  7102  eqsupti  7171  ordiso2  7210  enumctlemm  7289  enwomnilem  7344  cc2lem  7460  mulcanpig  7530  prarloclemlt  7688  genpdf  7703  genpdisj  7718  addnqprl  7724  addnqpru  7725  addlocpr  7731  prmuloc  7761  mulnqprl  7763  mulnqpru  7764  mullocpr  7766  ltpopr  7790  ltsopr  7791  ltaddpr  7792  ltexprlemdisj  7801  ltexprlemloc  7802  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  ltaprg  7814  recexprlemopu  7822  recexprlemloc  7826  cauappcvgprlemladdfl  7850  cauappcvgprlemladdru  7851  caucvgsrlemcau  7988  caucvgsrlemgt1  7990  caucvgsrlemoffcau  7993  caucvgsrlemoffres  7995  suplocsrlem  8003  axcaucvglemcau  8093  axpre-suploclemres  8096  axsuploc  8227  cnegexlem1  8329  cnegexlem3  8331  cnegex  8332  addsubeq4  8369  rimul  8740  divcanap6  8874  ltmul12a  9015  lemul12b  9016  lbinf  9103  zrevaddcl  9505  nzadd  9507  zextle  9546  fzind  9570  uz11  9753  infregelbex  9801  qreccl  9845  qrevaddcl  9847  irradd  9849  xrlttr  9999  xrltso  10000  xaddass  10073  xleadd1a  10077  xlt2add  10084  iccshftr  10198  iccshftl  10200  iccdil  10202  icccntr  10204  divelunit  10206  uzsubsubfz  10251  fzaddel  10263  fzrev  10288  elfzmlbp  10336  infssuzex  10461  zsupssdc  10466  frec2uzrdg  10639  frecuzrdgtcl  10642  frecuzrdgsuc  10644  frecuzrdgdomlem  10647  frecuzrdgfunlem  10649  frecuzrdgsuctlem  10653  iseqovex  10688  seq3val  10690  seqf  10694  seq3clss  10701  seq3fveq2  10705  seq3feq2  10706  seq3feq  10710  seq3shft2  10711  ser3mono  10717  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  seq3caopr2  10723  seqcaopr2g  10724  iseqf1olemab  10732  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  seq3f1olemstep  10744  seq3f1oleml  10746  seqf1oglem2a  10748  seqf1oglem2  10750  seq3id3  10754  seq3id  10755  seq3id2  10756  seq3homo  10757  seq3z  10758  seqfeq3  10759  seqhomog  10760  seqfeq4g  10761  ser3ge0  10766  expp1  10776  expnegap0  10777  expcllem  10780  mulexp  10808  expadd  10811  expaddzap  10813  expmulzap  10815  expdivap  10820  leexp1a  10824  expnlbnd  10894  bcpasc  10996  bccl  10997  hashfacen  11066  seq3coll  11072  ccatlen  11138  ccatvalfn  11144  ccatsymb  11145  pfxclz  11219  wrd2ind  11263  swrdccat  11275  seq3shft  11357  resqrexlemfp1  11528  sqrtdiv  11561  climshftlemg  11821  climcn1  11827  climsqz  11854  climsqz2  11855  clim2ser  11856  clim2ser2  11857  isermulc2  11859  climub  11863  serf0  11871  fsum3cvg  11897  sumrbdc  11898  summodclem3  11899  summodclem2a  11900  zsumdc  11903  fsumf1o  11909  isumss  11910  fisumss  11911  isumss2  11912  fsum3cvg2  11913  fsum3cvg3  11915  fsumcl2lem  11917  fsumcllem  11918  fsumadd  11925  fsumsplit  11926  fsumsplitsn  11929  sumsplitdc  11951  fisumrev2  11965  fsum2mul  11972  fsum00  11981  telfsumo  11985  fsumparts  11989  iserabs  11994  cvgratnnlemabsle  12046  cvgratnn  12050  cvgratz  12051  mertenslemub  12053  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  clim2prod  12058  clim2divap  12059  prodfap0  12064  prodfrecap  12065  prodeq2  12076  fproddccvg  12091  prodrbdclem2  12092  prodmodc  12097  zproddc  12098  fprodf1o  12107  fprodssdc  12109  fprodunsn  12123  fprodcllem  12125  fprodabs  12135  fprodeq0  12136  fprodmodd  12160  eftlcvg  12206  negdvdsb  12326  dvdsnegb  12327  fsumdvds  12361  dvdsext  12374  addmodlteqALT  12378  nno  12425  gcdsupex  12486  gcdsupcl  12487  bezoutlembz  12533  dvdssq  12560  eucalgf  12585  dvdslcm  12599  lcmledvds  12600  lcmeq0  12601  lcmcl  12602  lcmdvds  12609  lcmgcdeq  12613  divgcdcoprmex  12632  isprm5lem  12671  phibndlem  12746  phiprmpw  12752  pc2dvds  12861  pcmpt  12874  prmpwdvds  12886  1arith  12898  4sqleminfi  12928  ctiunctlemf  13017  ctiunct  13019  grpinva  13427  grprida  13428  gsumpropd2  13434  sgrppropd  13454  prdssgrpd  13456  mndpropd  13481  prdsidlem  13488  prdsmndd  13489  mhmpropd  13507  0mhm  13527  resmhm2  13529  resmhm2b  13530  grplcan  13603  mulgval  13667  mulgnn0z  13694  mulgnndir  13696  mulgnn0dir  13697  issubg2m  13734  issubg4m  13738  subgintm  13743  ghmf1  13818  gsumfzmptfidmadd  13884  gsumfzmhm  13888  srglmhm  13964  srgrmhm  13965  ringpropd  14009  crngpropd  14010  ringlghm  14032  ringrghm  14033  mulgass3  14056  issubrng2  14182  subrngpropd  14188  issubrg2  14213  subrgintm  14215  subrgpropd  14225  rhmpropd  14226  unitrrg  14239  lmodprop2d  14320  islss3  14351  lssintclm  14356  qusrhm  14500  gsumfzfsum  14560  opnssneib  14838  neissex  14847  tgrest  14851  iscnp3  14885  cnpnei  14901  cnrest  14917  tx1cn  14951  txcnp  14953  elbl3ps  15076  elbl3  15077  blininf  15106  blssexps  15111  blssex  15112  blpnfctr  15121  mopni2  15165  blsscls2  15175  metss  15176  bdmet  15184  metrest  15188  metcn  15196  txmetcn  15201  bl2ioo  15232  ivthinclemlr  15319  ivthinclemur  15321  dvcj  15391  dvfre  15392  elplyd  15423  plyaddlem1  15429  plymullem1  15430  plymullem  15432  plycolemc  15440  plycjlemc  15442  coseq0q4123  15516  abssinper  15528  fsumdvdsmul  15673  lgsval2lem  15697  lgsval4lem  15698  lgsneg  15711  lgsmod  15713  lgsdir2  15720  lgsdir  15722  lgsne0  15725  lgssq  15727  lgsquadlem1  15764  usgredg2vlem2  16029  subctctexmid  16395  cvgcmp2n  16431  iswomninnlem  16447  nconstwlpo  16464