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  3888  pofun  4327  ralxfrd  4477  rexxfrd  4478  ordtri2or2exmidlem  4540  wessep  4592  poinxp  4710  relop  4792  fun11iun  5498  ssimaex  5594  fndmdif  5638  fconst2g  5748  foeqcnvco  5808  f1eqcocnv  5809  isocnv  5829  isocnv2  5830  riota2df  5868  f1o2ndf1  6248  tfr1onlembacc  6362  tfr1onlemaccex  6368  tfr1onlemres  6369  tfrcllembacc  6375  tfrcllemaccex  6381  tfrcllemres  6382  tfrcldm  6383  tfrcl  6384  xpdom2  6850  fimax2gtrilemstep  6919  xpfi  6948  eqsupti  7015  ordiso2  7054  enumctlemm  7133  enwomnilem  7187  cc2lem  7285  mulcanpig  7354  prarloclemlt  7512  genpdf  7527  genpdisj  7542  addnqprl  7548  addnqpru  7549  addlocpr  7555  prmuloc  7585  mulnqprl  7587  mulnqpru  7588  mullocpr  7590  ltpopr  7614  ltsopr  7615  ltaddpr  7616  ltexprlemdisj  7625  ltexprlemloc  7626  ltexprlemru  7631  addcanprleml  7633  addcanprlemu  7634  ltaprg  7638  recexprlemopu  7646  recexprlemloc  7650  cauappcvgprlemladdfl  7674  cauappcvgprlemladdru  7675  caucvgsrlemcau  7812  caucvgsrlemgt1  7814  caucvgsrlemoffcau  7817  caucvgsrlemoffres  7819  suplocsrlem  7827  axcaucvglemcau  7917  axpre-suploclemres  7920  axsuploc  8050  cnegexlem1  8152  cnegexlem3  8154  cnegex  8155  addsubeq4  8192  rimul  8562  divcanap6  8696  ltmul12a  8837  lemul12b  8838  lbinf  8925  zrevaddcl  9323  nzadd  9325  zextle  9364  fzind  9388  uz11  9570  infregelbex  9618  qreccl  9662  qrevaddcl  9664  irradd  9666  xrlttr  9815  xrltso  9816  xaddass  9889  xleadd1a  9893  xlt2add  9900  iccshftr  10014  iccshftl  10016  iccdil  10018  icccntr  10020  divelunit  10022  uzsubsubfz  10067  fzaddel  10079  fzrev  10104  elfzmlbp  10152  frec2uzrdg  10429  frecuzrdgtcl  10432  frecuzrdgsuc  10434  frecuzrdgdomlem  10437  frecuzrdgfunlem  10439  frecuzrdgsuctlem  10443  iseqovex  10476  seq3val  10478  seqf  10481  seq3clss  10487  seq3fveq2  10489  seq3feq2  10490  seq3feq  10492  seq3shft2  10493  ser3mono  10498  seq3split  10499  seq3caopr3  10501  seq3caopr2  10502  iseqf1olemab  10509  seq3f1olemqsumkj  10518  seq3f1olemqsumk  10519  seq3f1olemqsum  10520  seq3f1olemstep  10521  seq3f1oleml  10523  seq3id3  10527  seq3id  10528  seq3id2  10529  seq3homo  10530  seq3z  10531  seqfeq3  10532  ser3ge0  10537  expp1  10547  expnegap0  10548  expcllem  10551  mulexp  10579  expadd  10582  expaddzap  10584  expmulzap  10586  expdivap  10591  leexp1a  10595  expnlbnd  10665  bcpasc  10766  bccl  10767  hashfacen  10836  seq3coll  10842  seq3shft  10867  resqrexlemfp1  11038  sqrtdiv  11071  climshftlemg  11330  climcn1  11336  climsqz  11363  climsqz2  11364  clim2ser  11365  clim2ser2  11366  isermulc2  11368  climub  11372  serf0  11380  fsum3cvg  11406  sumrbdc  11407  summodclem3  11408  summodclem2a  11409  zsumdc  11412  fsumf1o  11418  isumss  11419  fisumss  11420  isumss2  11421  fsum3cvg2  11422  fsum3cvg3  11424  fsumcl2lem  11426  fsumcllem  11427  fsumadd  11434  fsumsplit  11435  fsumsplitsn  11438  sumsplitdc  11460  fisumrev2  11474  fsum2mul  11481  fsum00  11490  telfsumo  11494  fsumparts  11498  iserabs  11503  cvgratnnlemabsle  11555  cvgratnn  11559  cvgratz  11560  mertenslemub  11562  mertenslemi1  11563  mertenslem2  11564  mertensabs  11565  clim2prod  11567  clim2divap  11568  prodfap0  11573  prodfrecap  11574  prodeq2  11585  fproddccvg  11600  prodrbdclem2  11601  prodmodc  11606  zproddc  11607  fprodf1o  11616  fprodssdc  11618  fprodunsn  11632  fprodcllem  11634  fprodabs  11644  fprodeq0  11645  fprodmodd  11669  eftlcvg  11715  negdvdsb  11834  dvdsnegb  11835  dvdsext  11881  addmodlteqALT  11885  nno  11931  infssuzex  11970  zsupssdc  11975  gcdsupex  11978  gcdsupcl  11979  bezoutlembz  12025  dvdssq  12052  eucalgf  12075  dvdslcm  12089  lcmledvds  12090  lcmeq0  12091  lcmcl  12092  lcmdvds  12099  lcmgcdeq  12103  divgcdcoprmex  12122  isprm5lem  12161  phibndlem  12236  phiprmpw  12242  pc2dvds  12349  pcmpt  12361  prmpwdvds  12373  1arith  12385  4sqleminfi  12415  ctiunctlemf  12464  ctiunct  12466  grpinva  12835  grprida  12836  sgrppropd  12849  mndpropd  12874  mhmpropd  12891  0mhm  12911  resmhm2  12913  resmhm2b  12914  grplcan  12979  mulgval  13037  mulgnn0z  13062  mulgnndir  13064  mulgnn0dir  13065  issubg2m  13101  issubg4m  13105  subgintm  13110  ghmf1  13180  srglmhm  13315  srgrmhm  13316  ringpropd  13360  crngpropd  13361  mulgass3  13403  issubrng2  13525  subrngpropd  13531  issubrg2  13556  subrgintm  13558  subrgpropd  13563  lmodprop2d  13632  islss3  13663  lssintclm  13668  opnssneib  14060  neissex  14069  tgrest  14073  iscnp3  14107  cnpnei  14123  cnrest  14139  tx1cn  14173  txcnp  14175  elbl3ps  14298  elbl3  14299  blininf  14328  blssexps  14333  blssex  14334  blpnfctr  14343  mopni2  14387  blsscls2  14397  metss  14398  bdmet  14406  metrest  14410  metcn  14418  txmetcn  14423  bl2ioo  14446  ivthinclemlr  14519  ivthinclemur  14521  dvcj  14577  dvfre  14578  coseq0q4123  14659  abssinper  14671  lgsval2lem  14815  lgsval4lem  14816  lgsneg  14829  lgsmod  14831  lgsdir2  14838  lgsdir  14840  lgsne0  14843  lgssq  14845  subctctexmid  15155  cvgcmp2n  15186  iswomninnlem  15202  nconstwlpo  15219