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  3857  intab  3955  pofun  4407  ralxfrd  4557  rexxfrd  4558  ordtri2or2exmidlem  4622  wessep  4674  poinxp  4793  relop  4878  fun11iun  5601  ssimaex  5703  fndmdif  5748  fconst2g  5864  foeqcnvco  5926  f1eqcocnv  5927  isocnv  5947  isocnv2  5948  riota2df  5988  caofdig  6264  f1o2ndf1  6388  tfr1onlembacc  6503  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllembacc  6516  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  tfrcl  6525  xpdom2  7010  fimax2gtrilemstep  7085  xpfi  7119  eqsupti  7189  ordiso2  7228  enumctlemm  7307  enwomnilem  7362  cc2lem  7478  mulcanpig  7548  prarloclemlt  7706  genpdf  7721  genpdisj  7736  addnqprl  7742  addnqpru  7743  addlocpr  7749  prmuloc  7779  mulnqprl  7781  mulnqpru  7782  mullocpr  7784  ltpopr  7808  ltsopr  7809  ltaddpr  7810  ltexprlemdisj  7819  ltexprlemloc  7820  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  ltaprg  7832  recexprlemopu  7840  recexprlemloc  7844  cauappcvgprlemladdfl  7868  cauappcvgprlemladdru  7869  caucvgsrlemcau  8006  caucvgsrlemgt1  8008  caucvgsrlemoffcau  8011  caucvgsrlemoffres  8013  suplocsrlem  8021  axcaucvglemcau  8111  axpre-suploclemres  8114  axsuploc  8245  cnegexlem1  8347  cnegexlem3  8349  cnegex  8350  addsubeq4  8387  rimul  8758  divcanap6  8892  ltmul12a  9033  lemul12b  9034  lbinf  9121  zrevaddcl  9523  nzadd  9525  zextle  9564  fzind  9588  uz11  9772  infregelbex  9825  qreccl  9869  qrevaddcl  9871  irradd  9873  xrlttr  10023  xrltso  10024  xaddass  10097  xleadd1a  10101  xlt2add  10108  iccshftr  10222  iccshftl  10224  iccdil  10226  icccntr  10228  divelunit  10230  uzsubsubfz  10275  fzaddel  10287  fzrev  10312  elfzmlbp  10360  infssuzex  10486  zsupssdc  10491  frec2uzrdg  10664  frecuzrdgtcl  10667  frecuzrdgsuc  10669  frecuzrdgdomlem  10672  frecuzrdgfunlem  10674  frecuzrdgsuctlem  10678  iseqovex  10713  seq3val  10715  seqf  10719  seq3clss  10726  seq3fveq2  10730  seq3feq2  10731  seq3feq  10735  seq3shft2  10736  ser3mono  10742  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  seq3caopr2  10748  seqcaopr2g  10749  iseqf1olemab  10757  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seq3f1olemqsum  10768  seq3f1olemstep  10769  seq3f1oleml  10771  seqf1oglem2a  10773  seqf1oglem2  10775  seq3id3  10779  seq3id  10780  seq3id2  10781  seq3homo  10782  seq3z  10783  seqfeq3  10784  seqhomog  10785  seqfeq4g  10786  ser3ge0  10791  expp1  10801  expnegap0  10802  expcllem  10805  mulexp  10833  expadd  10836  expaddzap  10838  expmulzap  10840  expdivap  10845  leexp1a  10849  expnlbnd  10919  bcpasc  11021  bccl  11022  hashfacen  11093  seq3coll  11099  ccatlen  11165  ccatvalfn  11171  ccatsymb  11172  ccatalpha  11183  pfxclz  11253  wrd2ind  11297  swrdccat  11309  seq3shft  11392  resqrexlemfp1  11563  sqrtdiv  11596  climshftlemg  11856  climcn1  11862  climsqz  11889  climsqz2  11890  clim2ser  11891  clim2ser2  11892  isermulc2  11894  climub  11898  serf0  11906  fsum3cvg  11932  sumrbdc  11933  summodclem3  11934  summodclem2a  11935  zsumdc  11938  fsumf1o  11944  isumss  11945  fisumss  11946  isumss2  11947  fsum3cvg2  11948  fsum3cvg3  11950  fsumcl2lem  11952  fsumcllem  11953  fsumadd  11960  fsumsplit  11961  fsumsplitsn  11964  sumsplitdc  11986  fisumrev2  12000  fsum2mul  12007  fsum00  12016  telfsumo  12020  fsumparts  12024  iserabs  12029  cvgratnnlemabsle  12081  cvgratnn  12085  cvgratz  12086  mertenslemub  12088  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  clim2prod  12093  clim2divap  12094  prodfap0  12099  prodfrecap  12100  prodeq2  12111  fproddccvg  12126  prodrbdclem2  12127  prodmodc  12132  zproddc  12133  fprodf1o  12142  fprodssdc  12144  fprodunsn  12158  fprodcllem  12160  fprodabs  12170  fprodeq0  12171  fprodmodd  12195  eftlcvg  12241  negdvdsb  12361  dvdsnegb  12362  fsumdvds  12396  dvdsext  12409  addmodlteqALT  12413  nno  12460  gcdsupex  12521  gcdsupcl  12522  bezoutlembz  12568  dvdssq  12595  eucalgf  12620  dvdslcm  12634  lcmledvds  12635  lcmeq0  12636  lcmcl  12637  lcmdvds  12644  lcmgcdeq  12648  divgcdcoprmex  12667  isprm5lem  12706  phibndlem  12781  phiprmpw  12787  pc2dvds  12896  pcmpt  12909  prmpwdvds  12921  1arith  12933  4sqleminfi  12963  ctiunctlemf  13052  ctiunct  13054  grpinva  13462  grprida  13463  gsumpropd2  13469  sgrppropd  13489  prdssgrpd  13491  mndpropd  13516  prdsidlem  13523  prdsmndd  13524  mhmpropd  13542  0mhm  13562  resmhm2  13564  resmhm2b  13565  grplcan  13638  mulgval  13702  mulgnn0z  13729  mulgnndir  13731  mulgnn0dir  13732  issubg2m  13769  issubg4m  13773  subgintm  13778  ghmf1  13853  gsumfzmptfidmadd  13919  gsumfzmhm  13923  srglmhm  13999  srgrmhm  14000  ringpropd  14044  crngpropd  14045  ringlghm  14067  ringrghm  14068  mulgass3  14091  issubrng2  14217  subrngpropd  14223  issubrg2  14248  subrgintm  14250  subrgpropd  14260  rhmpropd  14261  unitrrg  14274  lmodprop2d  14355  islss3  14386  lssintclm  14391  qusrhm  14535  gsumfzfsum  14595  opnssneib  14873  neissex  14882  tgrest  14886  iscnp3  14920  cnpnei  14936  cnrest  14952  tx1cn  14986  txcnp  14988  elbl3ps  15111  elbl3  15112  blininf  15141  blssexps  15146  blssex  15147  blpnfctr  15156  mopni2  15200  blsscls2  15210  metss  15211  bdmet  15219  metrest  15223  metcn  15231  txmetcn  15236  bl2ioo  15267  ivthinclemlr  15354  ivthinclemur  15356  dvcj  15426  dvfre  15427  elplyd  15458  plyaddlem1  15464  plymullem1  15465  plymullem  15467  plycolemc  15475  plycjlemc  15477  coseq0q4123  15551  abssinper  15563  fsumdvdsmul  15708  lgsval2lem  15732  lgsval4lem  15733  lgsneg  15746  lgsmod  15748  lgsdir2  15755  lgsdir  15757  lgsne0  15760  lgssq  15762  lgsquadlem1  15799  usgredg2vlem2  16067  clwwlkccat  16210  clwwlknonex2lem2  16247  subctctexmid  16551  cvgcmp2n  16587  iswomninnlem  16603  nconstwlpo  16620