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  1160  3ad2antl2  1161  ad4ant124  1217  3adant1r  1232  ad5ant235  1239  ad5ant135  1244  bilukdc  1406  intab  3885  pofun  4324  ralxfrd  4474  rexxfrd  4475  ordtri2or2exmidlem  4537  wessep  4589  poinxp  4707  relop  4789  fun11iun  5494  ssimaex  5590  fndmdif  5634  fconst2g  5744  foeqcnvco  5804  f1eqcocnv  5805  isocnv  5825  isocnv2  5826  riota2df  5864  f1o2ndf1  6243  tfr1onlembacc  6357  tfr1onlemaccex  6363  tfr1onlemres  6364  tfrcllembacc  6370  tfrcllemaccex  6376  tfrcllemres  6377  tfrcldm  6378  tfrcl  6379  xpdom2  6845  fimax2gtrilemstep  6914  xpfi  6943  eqsupti  7009  ordiso2  7048  enumctlemm  7127  enwomnilem  7181  cc2lem  7279  mulcanpig  7348  prarloclemlt  7506  genpdf  7521  genpdisj  7536  addnqprl  7542  addnqpru  7543  addlocpr  7549  prmuloc  7579  mulnqprl  7581  mulnqpru  7582  mullocpr  7584  ltpopr  7608  ltsopr  7609  ltaddpr  7610  ltexprlemdisj  7619  ltexprlemloc  7620  ltexprlemru  7625  addcanprleml  7627  addcanprlemu  7628  ltaprg  7632  recexprlemopu  7640  recexprlemloc  7644  cauappcvgprlemladdfl  7668  cauappcvgprlemladdru  7669  caucvgsrlemcau  7806  caucvgsrlemgt1  7808  caucvgsrlemoffcau  7811  caucvgsrlemoffres  7813  suplocsrlem  7821  axcaucvglemcau  7911  axpre-suploclemres  7914  axsuploc  8044  cnegexlem1  8146  cnegexlem3  8148  cnegex  8149  addsubeq4  8186  rimul  8556  divcanap6  8690  ltmul12a  8831  lemul12b  8832  lbinf  8919  zrevaddcl  9317  nzadd  9319  zextle  9358  fzind  9382  uz11  9564  infregelbex  9612  qreccl  9656  qrevaddcl  9658  irradd  9660  xrlttr  9809  xrltso  9810  xaddass  9883  xleadd1a  9887  xlt2add  9894  iccshftr  10008  iccshftl  10010  iccdil  10012  icccntr  10014  divelunit  10016  uzsubsubfz  10061  fzaddel  10073  fzrev  10098  elfzmlbp  10146  frec2uzrdg  10423  frecuzrdgtcl  10426  frecuzrdgsuc  10428  frecuzrdgdomlem  10431  frecuzrdgfunlem  10433  frecuzrdgsuctlem  10437  iseqovex  10470  seq3val  10472  seqf  10475  seq3clss  10481  seq3fveq2  10483  seq3feq2  10484  seq3feq  10486  seq3shft2  10487  ser3mono  10492  seq3split  10493  seq3caopr3  10495  seq3caopr2  10496  iseqf1olemab  10503  seq3f1olemqsumkj  10512  seq3f1olemqsumk  10513  seq3f1olemqsum  10514  seq3f1olemstep  10515  seq3f1oleml  10517  seq3id3  10521  seq3id  10522  seq3id2  10523  seq3homo  10524  seq3z  10525  seqfeq3  10526  ser3ge0  10531  expp1  10541  expnegap0  10542  expcllem  10545  mulexp  10573  expadd  10576  expaddzap  10578  expmulzap  10580  expdivap  10585  leexp1a  10589  expnlbnd  10659  bcpasc  10760  bccl  10761  hashfacen  10830  seq3coll  10836  seq3shft  10861  resqrexlemfp1  11032  sqrtdiv  11065  climshftlemg  11324  climcn1  11330  climsqz  11357  climsqz2  11358  clim2ser  11359  clim2ser2  11360  isermulc2  11362  climub  11366  serf0  11374  fsum3cvg  11400  sumrbdc  11401  summodclem3  11402  summodclem2a  11403  zsumdc  11406  fsumf1o  11412  isumss  11413  fisumss  11414  isumss2  11415  fsum3cvg2  11416  fsum3cvg3  11418  fsumcl2lem  11420  fsumcllem  11421  fsumadd  11428  fsumsplit  11429  fsumsplitsn  11432  sumsplitdc  11454  fisumrev2  11468  fsum2mul  11475  fsum00  11484  telfsumo  11488  fsumparts  11492  iserabs  11497  cvgratnnlemabsle  11549  cvgratnn  11553  cvgratz  11554  mertenslemub  11556  mertenslemi1  11557  mertenslem2  11558  mertensabs  11559  clim2prod  11561  clim2divap  11562  prodfap0  11567  prodfrecap  11568  prodeq2  11579  fproddccvg  11594  prodrbdclem2  11595  prodmodc  11600  zproddc  11601  fprodf1o  11610  fprodssdc  11612  fprodunsn  11626  fprodcllem  11628  fprodabs  11638  fprodeq0  11639  fprodmodd  11663  eftlcvg  11709  negdvdsb  11828  dvdsnegb  11829  dvdsext  11875  addmodlteqALT  11879  nno  11925  infssuzex  11964  zsupssdc  11969  gcdsupex  11972  gcdsupcl  11973  bezoutlembz  12019  dvdssq  12046  eucalgf  12069  dvdslcm  12083  lcmledvds  12084  lcmeq0  12085  lcmcl  12086  lcmdvds  12093  lcmgcdeq  12097  divgcdcoprmex  12116  isprm5lem  12155  phibndlem  12230  phiprmpw  12236  pc2dvds  12343  pcmpt  12355  prmpwdvds  12367  1arith  12379  ctiunctlemf  12453  ctiunct  12455  grpinva  12824  grprida  12825  sgrppropd  12838  mndpropd  12863  mhmpropd  12879  0mhm  12895  grplcan  12959  mulgval  13017  mulgnn0z  13042  mulgnndir  13044  mulgnn0dir  13045  issubg2m  13081  issubg4m  13085  subgintm  13090  srglmhm  13245  srgrmhm  13246  ringpropd  13290  crngpropd  13291  mulgass3  13333  issubrng2  13430  subrngpropd  13436  issubrg2  13461  subrgintm  13463  subrgpropd  13468  lmodprop2d  13537  islss3  13568  lssintclm  13573  opnssneib  13952  neissex  13961  tgrest  13965  iscnp3  13999  cnpnei  14015  cnrest  14031  tx1cn  14065  txcnp  14067  elbl3ps  14190  elbl3  14191  blininf  14220  blssexps  14225  blssex  14226  blpnfctr  14235  mopni2  14279  blsscls2  14289  metss  14290  bdmet  14298  metrest  14302  metcn  14310  txmetcn  14315  bl2ioo  14338  ivthinclemlr  14411  ivthinclemur  14413  dvcj  14469  dvfre  14470  coseq0q4123  14551  abssinper  14563  lgsval2lem  14707  lgsval4lem  14708  lgsneg  14721  lgsmod  14723  lgsdir2  14730  lgsdir  14732  lgsne0  14735  lgssq  14737  subctctexmid  15047  cvgcmp2n  15078  iswomninnlem  15094  nconstwlpo  15111