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  3904  pofun  4348  ralxfrd  4498  rexxfrd  4499  ordtri2or2exmidlem  4563  wessep  4615  poinxp  4733  relop  4817  fun11iun  5528  ssimaex  5625  fndmdif  5670  fconst2g  5780  foeqcnvco  5840  f1eqcocnv  5841  isocnv  5861  isocnv2  5862  riota2df  5901  caofdig  6173  f1o2ndf1  6295  tfr1onlembacc  6409  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllembacc  6422  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  tfrcl  6431  xpdom2  6899  fimax2gtrilemstep  6970  xpfi  7002  eqsupti  7071  ordiso2  7110  enumctlemm  7189  enwomnilem  7244  cc2lem  7351  mulcanpig  7421  prarloclemlt  7579  genpdf  7594  genpdisj  7609  addnqprl  7615  addnqpru  7616  addlocpr  7622  prmuloc  7652  mulnqprl  7654  mulnqpru  7655  mullocpr  7657  ltpopr  7681  ltsopr  7682  ltaddpr  7683  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  ltaprg  7705  recexprlemopu  7713  recexprlemloc  7717  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  suplocsrlem  7894  axcaucvglemcau  7984  axpre-suploclemres  7987  axsuploc  8118  cnegexlem1  8220  cnegexlem3  8222  cnegex  8223  addsubeq4  8260  rimul  8631  divcanap6  8765  ltmul12a  8906  lemul12b  8907  lbinf  8994  zrevaddcl  9395  nzadd  9397  zextle  9436  fzind  9460  uz11  9643  infregelbex  9691  qreccl  9735  qrevaddcl  9737  irradd  9739  xrlttr  9889  xrltso  9890  xaddass  9963  xleadd1a  9967  xlt2add  9974  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  divelunit  10096  uzsubsubfz  10141  fzaddel  10153  fzrev  10178  elfzmlbp  10226  infssuzex  10342  zsupssdc  10347  frec2uzrdg  10520  frecuzrdgtcl  10523  frecuzrdgsuc  10525  frecuzrdgdomlem  10528  frecuzrdgfunlem  10530  frecuzrdgsuctlem  10534  iseqovex  10569  seq3val  10571  seqf  10575  seq3clss  10582  seq3fveq2  10586  seq3feq2  10587  seq3feq  10591  seq3shft2  10592  ser3mono  10598  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seq3caopr2  10604  seqcaopr2g  10605  iseqf1olemab  10613  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemstep  10625  seq3f1oleml  10627  seqf1oglem2a  10629  seqf1oglem2  10631  seq3id3  10635  seq3id  10636  seq3id2  10637  seq3homo  10638  seq3z  10639  seqfeq3  10640  seqhomog  10641  seqfeq4g  10642  ser3ge0  10647  expp1  10657  expnegap0  10658  expcllem  10661  mulexp  10689  expadd  10692  expaddzap  10694  expmulzap  10696  expdivap  10701  leexp1a  10705  expnlbnd  10775  bcpasc  10877  bccl  10878  hashfacen  10947  seq3coll  10953  seq3shft  11022  resqrexlemfp1  11193  sqrtdiv  11226  climshftlemg  11486  climcn1  11492  climsqz  11519  climsqz2  11520  clim2ser  11521  clim2ser2  11522  isermulc2  11524  climub  11528  serf0  11536  fsum3cvg  11562  sumrbdc  11563  summodclem3  11564  summodclem2a  11565  zsumdc  11568  fsumf1o  11574  isumss  11575  fisumss  11576  isumss2  11577  fsum3cvg2  11578  fsum3cvg3  11580  fsumcl2lem  11582  fsumcllem  11583  fsumadd  11590  fsumsplit  11591  fsumsplitsn  11594  sumsplitdc  11616  fisumrev2  11630  fsum2mul  11637  fsum00  11646  telfsumo  11650  fsumparts  11654  iserabs  11659  cvgratnnlemabsle  11711  cvgratnn  11715  cvgratz  11716  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  clim2prod  11723  clim2divap  11724  prodfap0  11729  prodfrecap  11730  prodeq2  11741  fproddccvg  11756  prodrbdclem2  11757  prodmodc  11762  zproddc  11763  fprodf1o  11772  fprodssdc  11774  fprodunsn  11788  fprodcllem  11790  fprodabs  11800  fprodeq0  11801  fprodmodd  11825  eftlcvg  11871  negdvdsb  11991  dvdsnegb  11992  fsumdvds  12026  dvdsext  12039  addmodlteqALT  12043  nno  12090  gcdsupex  12151  gcdsupcl  12152  bezoutlembz  12198  dvdssq  12225  eucalgf  12250  dvdslcm  12264  lcmledvds  12265  lcmeq0  12266  lcmcl  12267  lcmdvds  12274  lcmgcdeq  12278  divgcdcoprmex  12297  isprm5lem  12336  phibndlem  12411  phiprmpw  12417  pc2dvds  12526  pcmpt  12539  prmpwdvds  12551  1arith  12563  4sqleminfi  12593  ctiunctlemf  12682  ctiunct  12684  grpinva  13090  grprida  13091  gsumpropd2  13097  sgrppropd  13117  prdssgrpd  13119  mndpropd  13144  prdsidlem  13151  prdsmndd  13152  mhmpropd  13170  0mhm  13190  resmhm2  13192  resmhm2b  13193  grplcan  13266  mulgval  13330  mulgnn0z  13357  mulgnndir  13359  mulgnn0dir  13360  issubg2m  13397  issubg4m  13401  subgintm  13406  ghmf1  13481  gsumfzmptfidmadd  13547  gsumfzmhm  13551  srglmhm  13627  srgrmhm  13628  ringpropd  13672  crngpropd  13673  ringlghm  13695  ringrghm  13696  mulgass3  13719  issubrng2  13844  subrngpropd  13850  issubrg2  13875  subrgintm  13877  subrgpropd  13887  rhmpropd  13888  unitrrg  13901  lmodprop2d  13982  islss3  14013  lssintclm  14018  qusrhm  14162  gsumfzfsum  14222  opnssneib  14478  neissex  14487  tgrest  14491  iscnp3  14525  cnpnei  14541  cnrest  14557  tx1cn  14591  txcnp  14593  elbl3ps  14716  elbl3  14717  blininf  14746  blssexps  14751  blssex  14752  blpnfctr  14761  mopni2  14805  blsscls2  14815  metss  14816  bdmet  14824  metrest  14828  metcn  14836  txmetcn  14841  bl2ioo  14872  ivthinclemlr  14959  ivthinclemur  14961  dvcj  15031  dvfre  15032  elplyd  15063  plyaddlem1  15069  plymullem1  15070  plymullem  15072  plycolemc  15080  plycjlemc  15082  coseq0q4123  15156  abssinper  15168  fsumdvdsmul  15313  lgsval2lem  15337  lgsval4lem  15338  lgsneg  15351  lgsmod  15353  lgsdir2  15360  lgsdir  15362  lgsne0  15365  lgssq  15367  lgsquadlem1  15404  subctctexmid  15733  cvgcmp2n  15768  iswomninnlem  15784  nconstwlpo  15801