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  1164  3ad2antl2  1165  ad4ant124  1221  3adant1r  1236  ad5ant235  1243  ad5ant135  1248  bilukdc  1418  elpr2elpr  3833  intab  3931  pofun  4380  ralxfrd  4530  rexxfrd  4531  ordtri2or2exmidlem  4595  wessep  4647  poinxp  4765  relop  4849  fun11iun  5569  ssimaex  5668  fndmdif  5713  fconst2g  5827  foeqcnvco  5887  f1eqcocnv  5888  isocnv  5908  isocnv2  5909  riota2df  5949  caofdig  6222  f1o2ndf1  6344  tfr1onlembacc  6458  tfr1onlemaccex  6464  tfr1onlemres  6465  tfrcllembacc  6471  tfrcllemaccex  6477  tfrcllemres  6478  tfrcldm  6479  tfrcl  6480  xpdom2  6958  fimax2gtrilemstep  7030  xpfi  7062  eqsupti  7131  ordiso2  7170  enumctlemm  7249  enwomnilem  7304  cc2lem  7420  mulcanpig  7490  prarloclemlt  7648  genpdf  7663  genpdisj  7678  addnqprl  7684  addnqpru  7685  addlocpr  7691  prmuloc  7721  mulnqprl  7723  mulnqpru  7724  mullocpr  7726  ltpopr  7750  ltsopr  7751  ltaddpr  7752  ltexprlemdisj  7761  ltexprlemloc  7762  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  ltaprg  7774  recexprlemopu  7782  recexprlemloc  7786  cauappcvgprlemladdfl  7810  cauappcvgprlemladdru  7811  caucvgsrlemcau  7948  caucvgsrlemgt1  7950  caucvgsrlemoffcau  7953  caucvgsrlemoffres  7955  suplocsrlem  7963  axcaucvglemcau  8053  axpre-suploclemres  8056  axsuploc  8187  cnegexlem1  8289  cnegexlem3  8291  cnegex  8292  addsubeq4  8329  rimul  8700  divcanap6  8834  ltmul12a  8975  lemul12b  8976  lbinf  9063  zrevaddcl  9465  nzadd  9467  zextle  9506  fzind  9530  uz11  9713  infregelbex  9761  qreccl  9805  qrevaddcl  9807  irradd  9809  xrlttr  9959  xrltso  9960  xaddass  10033  xleadd1a  10037  xlt2add  10044  iccshftr  10158  iccshftl  10160  iccdil  10162  icccntr  10164  divelunit  10166  uzsubsubfz  10211  fzaddel  10223  fzrev  10248  elfzmlbp  10296  infssuzex  10420  zsupssdc  10425  frec2uzrdg  10598  frecuzrdgtcl  10601  frecuzrdgsuc  10603  frecuzrdgdomlem  10606  frecuzrdgfunlem  10608  frecuzrdgsuctlem  10612  iseqovex  10647  seq3val  10649  seqf  10653  seq3clss  10660  seq3fveq2  10664  seq3feq2  10665  seq3feq  10669  seq3shft2  10670  ser3mono  10676  seq3split  10677  seqsplitg  10678  seq3caopr3  10680  seq3caopr2  10682  seqcaopr2g  10683  iseqf1olemab  10691  seq3f1olemqsumkj  10700  seq3f1olemqsumk  10701  seq3f1olemqsum  10702  seq3f1olemstep  10703  seq3f1oleml  10705  seqf1oglem2a  10707  seqf1oglem2  10709  seq3id3  10713  seq3id  10714  seq3id2  10715  seq3homo  10716  seq3z  10717  seqfeq3  10718  seqhomog  10719  seqfeq4g  10720  ser3ge0  10725  expp1  10735  expnegap0  10736  expcllem  10739  mulexp  10767  expadd  10770  expaddzap  10772  expmulzap  10774  expdivap  10779  leexp1a  10783  expnlbnd  10853  bcpasc  10955  bccl  10956  hashfacen  11025  seq3coll  11031  ccatlen  11096  ccatvalfn  11102  ccatsymb  11103  pfxclz  11177  wrd2ind  11221  swrdccat  11233  seq3shft  11315  resqrexlemfp1  11486  sqrtdiv  11519  climshftlemg  11779  climcn1  11785  climsqz  11812  climsqz2  11813  clim2ser  11814  clim2ser2  11815  isermulc2  11817  climub  11821  serf0  11829  fsum3cvg  11855  sumrbdc  11856  summodclem3  11857  summodclem2a  11858  zsumdc  11861  fsumf1o  11867  isumss  11868  fisumss  11869  isumss2  11870  fsum3cvg2  11871  fsum3cvg3  11873  fsumcl2lem  11875  fsumcllem  11876  fsumadd  11883  fsumsplit  11884  fsumsplitsn  11887  sumsplitdc  11909  fisumrev2  11923  fsum2mul  11930  fsum00  11939  telfsumo  11943  fsumparts  11947  iserabs  11952  cvgratnnlemabsle  12004  cvgratnn  12008  cvgratz  12009  mertenslemub  12011  mertenslemi1  12012  mertenslem2  12013  mertensabs  12014  clim2prod  12016  clim2divap  12017  prodfap0  12022  prodfrecap  12023  prodeq2  12034  fproddccvg  12049  prodrbdclem2  12050  prodmodc  12055  zproddc  12056  fprodf1o  12065  fprodssdc  12067  fprodunsn  12081  fprodcllem  12083  fprodabs  12093  fprodeq0  12094  fprodmodd  12118  eftlcvg  12164  negdvdsb  12284  dvdsnegb  12285  fsumdvds  12319  dvdsext  12332  addmodlteqALT  12336  nno  12383  gcdsupex  12444  gcdsupcl  12445  bezoutlembz  12491  dvdssq  12518  eucalgf  12543  dvdslcm  12557  lcmledvds  12558  lcmeq0  12559  lcmcl  12560  lcmdvds  12567  lcmgcdeq  12571  divgcdcoprmex  12590  isprm5lem  12629  phibndlem  12704  phiprmpw  12710  pc2dvds  12819  pcmpt  12832  prmpwdvds  12844  1arith  12856  4sqleminfi  12886  ctiunctlemf  12975  ctiunct  12977  grpinva  13385  grprida  13386  gsumpropd2  13392  sgrppropd  13412  prdssgrpd  13414  mndpropd  13439  prdsidlem  13446  prdsmndd  13447  mhmpropd  13465  0mhm  13485  resmhm2  13487  resmhm2b  13488  grplcan  13561  mulgval  13625  mulgnn0z  13652  mulgnndir  13654  mulgnn0dir  13655  issubg2m  13692  issubg4m  13696  subgintm  13701  ghmf1  13776  gsumfzmptfidmadd  13842  gsumfzmhm  13846  srglmhm  13922  srgrmhm  13923  ringpropd  13967  crngpropd  13968  ringlghm  13990  ringrghm  13991  mulgass3  14014  issubrng2  14139  subrngpropd  14145  issubrg2  14170  subrgintm  14172  subrgpropd  14182  rhmpropd  14183  unitrrg  14196  lmodprop2d  14277  islss3  14308  lssintclm  14313  qusrhm  14457  gsumfzfsum  14517  opnssneib  14795  neissex  14804  tgrest  14808  iscnp3  14842  cnpnei  14858  cnrest  14874  tx1cn  14908  txcnp  14910  elbl3ps  15033  elbl3  15034  blininf  15063  blssexps  15068  blssex  15069  blpnfctr  15078  mopni2  15122  blsscls2  15132  metss  15133  bdmet  15141  metrest  15145  metcn  15153  txmetcn  15158  bl2ioo  15189  ivthinclemlr  15276  ivthinclemur  15278  dvcj  15348  dvfre  15349  elplyd  15380  plyaddlem1  15386  plymullem1  15387  plymullem  15389  plycolemc  15397  plycjlemc  15399  coseq0q4123  15473  abssinper  15485  fsumdvdsmul  15630  lgsval2lem  15654  lgsval4lem  15655  lgsneg  15668  lgsmod  15670  lgsdir2  15677  lgsdir  15679  lgsne0  15682  lgssq  15684  lgsquadlem1  15721  usgredg2vlem2  15986  subctctexmid  16277  cvgcmp2n  16312  iswomninnlem  16328  nconstwlpo  16345