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  1159  3ad2antl2  1160  ad4ant124  1216  3adant1r  1231  bilukdc  1396  intab  3875  pofun  4314  ralxfrd  4464  rexxfrd  4465  ordtri2or2exmidlem  4527  wessep  4579  poinxp  4697  relop  4779  fun11iun  5484  ssimaex  5579  fndmdif  5623  fconst2g  5733  foeqcnvco  5793  f1eqcocnv  5794  isocnv  5814  isocnv2  5815  riota2df  5853  f1o2ndf1  6231  tfr1onlembacc  6345  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllembacc  6358  tfrcllemaccex  6364  tfrcllemres  6365  tfrcldm  6366  tfrcl  6367  xpdom2  6833  fimax2gtrilemstep  6902  xpfi  6931  eqsupti  6997  ordiso2  7036  enumctlemm  7115  enwomnilem  7169  cc2lem  7267  mulcanpig  7336  prarloclemlt  7494  genpdf  7509  genpdisj  7524  addnqprl  7530  addnqpru  7531  addlocpr  7537  prmuloc  7567  mulnqprl  7569  mulnqpru  7570  mullocpr  7572  ltpopr  7596  ltsopr  7597  ltaddpr  7598  ltexprlemdisj  7607  ltexprlemloc  7608  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  ltaprg  7620  recexprlemopu  7628  recexprlemloc  7632  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  caucvgsrlemcau  7794  caucvgsrlemgt1  7796  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  suplocsrlem  7809  axcaucvglemcau  7899  axpre-suploclemres  7902  axsuploc  8032  cnegexlem1  8134  cnegexlem3  8136  cnegex  8137  addsubeq4  8174  rimul  8544  divcanap6  8678  ltmul12a  8819  lemul12b  8820  lbinf  8907  zrevaddcl  9305  nzadd  9307  zextle  9346  fzind  9370  uz11  9552  infregelbex  9600  qreccl  9644  qrevaddcl  9646  irradd  9648  xrlttr  9797  xrltso  9798  xaddass  9871  xleadd1a  9875  xlt2add  9882  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  divelunit  10004  uzsubsubfz  10049  fzaddel  10061  fzrev  10086  elfzmlbp  10134  frec2uzrdg  10411  frecuzrdgtcl  10414  frecuzrdgsuc  10416  frecuzrdgdomlem  10419  frecuzrdgfunlem  10421  frecuzrdgsuctlem  10425  iseqovex  10458  seq3val  10460  seqf  10463  seq3clss  10469  seq3fveq2  10471  seq3feq2  10472  seq3feq  10474  seq3shft2  10475  ser3mono  10480  seq3split  10481  seq3caopr3  10483  seq3caopr2  10484  iseqf1olemab  10491  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1olemstep  10503  seq3f1oleml  10505  seq3id3  10509  seq3id  10510  seq3id2  10511  seq3homo  10512  seq3z  10513  seqfeq3  10514  ser3ge0  10519  expp1  10529  expnegap0  10530  expcllem  10533  mulexp  10561  expadd  10564  expaddzap  10566  expmulzap  10568  expdivap  10573  leexp1a  10577  expnlbnd  10647  bcpasc  10748  bccl  10749  hashfacen  10818  seq3coll  10824  seq3shft  10849  resqrexlemfp1  11020  sqrtdiv  11053  climshftlemg  11312  climcn1  11318  climsqz  11345  climsqz2  11346  clim2ser  11347  clim2ser2  11348  isermulc2  11350  climub  11354  serf0  11362  fsum3cvg  11388  sumrbdc  11389  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsumf1o  11400  isumss  11401  fisumss  11402  isumss2  11403  fsum3cvg2  11404  fsum3cvg3  11406  fsumcl2lem  11408  fsumcllem  11409  fsumadd  11416  fsumsplit  11417  fsumsplitsn  11420  sumsplitdc  11442  fisumrev2  11456  fsum2mul  11463  fsum00  11472  telfsumo  11476  fsumparts  11480  iserabs  11485  cvgratnnlemabsle  11537  cvgratnn  11541  cvgratz  11542  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  clim2prod  11549  clim2divap  11550  prodfap0  11555  prodfrecap  11556  prodeq2  11567  fproddccvg  11582  prodrbdclem2  11583  prodmodc  11588  zproddc  11589  fprodf1o  11598  fprodssdc  11600  fprodunsn  11614  fprodcllem  11616  fprodabs  11626  fprodeq0  11627  fprodmodd  11651  eftlcvg  11697  negdvdsb  11816  dvdsnegb  11817  dvdsext  11863  addmodlteqALT  11867  nno  11913  infssuzex  11952  zsupssdc  11957  gcdsupex  11960  gcdsupcl  11961  bezoutlembz  12007  dvdssq  12034  eucalgf  12057  dvdslcm  12071  lcmledvds  12072  lcmeq0  12073  lcmcl  12074  lcmdvds  12081  lcmgcdeq  12085  divgcdcoprmex  12104  isprm5lem  12143  phibndlem  12218  phiprmpw  12224  pc2dvds  12331  pcmpt  12343  prmpwdvds  12355  1arith  12367  ctiunctlemf  12441  ctiunct  12443  grprinvd  12810  grpridd  12811  mndpropd  12846  mhmpropd  12862  0mhm  12878  grplcan  12937  mulgval  12991  mulgnn0z  13015  mulgnndir  13017  mulgnn0dir  13018  issubg2m  13054  issubg4m  13058  subgintm  13063  srglmhm  13181  srgrmhm  13182  ringpropd  13222  crngpropd  13223  mulgass3  13259  issubrg2  13367  subrgintm  13369  subrgpropd  13374  lmodprop2d  13443  islss3  13471  lssintclm  13476  opnssneib  13695  neissex  13704  tgrest  13708  iscnp3  13742  cnpnei  13758  cnrest  13774  tx1cn  13808  txcnp  13810  elbl3ps  13933  elbl3  13934  blininf  13963  blssexps  13968  blssex  13969  blpnfctr  13978  mopni2  14022  blsscls2  14032  metss  14033  bdmet  14041  metrest  14045  metcn  14053  txmetcn  14058  bl2ioo  14081  ivthinclemlr  14154  ivthinclemur  14156  dvcj  14212  dvfre  14213  coseq0q4123  14294  abssinper  14306  lgsval2lem  14450  lgsval4lem  14451  lgsneg  14464  lgsmod  14466  lgsdir2  14473  lgsdir  14475  lgsne0  14478  lgssq  14480  subctctexmid  14789  cvgcmp2n  14820  iswomninnlem  14836  nconstwlpo  14853