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  3869  pofun  4306  ralxfrd  4456  rexxfrd  4457  ordtri2or2exmidlem  4519  wessep  4571  poinxp  4689  relop  4770  fun11iun  5474  ssimaex  5569  fndmdif  5613  fconst2g  5723  foeqcnvco  5781  f1eqcocnv  5782  isocnv  5802  isocnv2  5803  riota2df  5841  f1o2ndf1  6219  tfr1onlembacc  6333  tfr1onlemaccex  6339  tfr1onlemres  6340  tfrcllembacc  6346  tfrcllemaccex  6352  tfrcllemres  6353  tfrcldm  6354  tfrcl  6355  xpdom2  6821  fimax2gtrilemstep  6890  xpfi  6919  eqsupti  6985  ordiso2  7024  enumctlemm  7103  enwomnilem  7157  cc2lem  7240  mulcanpig  7309  prarloclemlt  7467  genpdf  7482  genpdisj  7497  addnqprl  7503  addnqpru  7504  addlocpr  7510  prmuloc  7540  mulnqprl  7542  mulnqpru  7543  mullocpr  7545  ltpopr  7569  ltsopr  7570  ltaddpr  7571  ltexprlemdisj  7580  ltexprlemloc  7581  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  ltaprg  7593  recexprlemopu  7601  recexprlemloc  7605  cauappcvgprlemladdfl  7629  cauappcvgprlemladdru  7630  caucvgsrlemcau  7767  caucvgsrlemgt1  7769  caucvgsrlemoffcau  7772  caucvgsrlemoffres  7774  suplocsrlem  7782  axcaucvglemcau  7872  axpre-suploclemres  7875  axsuploc  8004  cnegexlem1  8106  cnegexlem3  8108  cnegex  8109  addsubeq4  8146  rimul  8516  divcanap6  8649  ltmul12a  8790  lemul12b  8791  lbinf  8878  zrevaddcl  9276  nzadd  9278  zextle  9317  fzind  9341  uz11  9523  infregelbex  9571  qreccl  9615  qrevaddcl  9617  irradd  9619  xrlttr  9766  xrltso  9767  xaddass  9840  xleadd1a  9844  xlt2add  9851  iccshftr  9965  iccshftl  9967  iccdil  9969  icccntr  9971  divelunit  9973  uzsubsubfz  10017  fzaddel  10029  fzrev  10054  elfzmlbp  10102  frec2uzrdg  10379  frecuzrdgtcl  10382  frecuzrdgsuc  10384  frecuzrdgdomlem  10387  frecuzrdgfunlem  10389  frecuzrdgsuctlem  10393  iseqovex  10426  seq3val  10428  seqf  10431  seq3clss  10437  seq3fveq2  10439  seq3feq2  10440  seq3feq  10442  seq3shft2  10443  ser3mono  10448  seq3split  10449  seq3caopr3  10451  seq3caopr2  10452  iseqf1olemab  10459  seq3f1olemqsumkj  10468  seq3f1olemqsumk  10469  seq3f1olemqsum  10470  seq3f1olemstep  10471  seq3f1oleml  10473  seq3id3  10477  seq3id  10478  seq3id2  10479  seq3homo  10480  seq3z  10481  seqfeq3  10482  ser3ge0  10487  expp1  10497  expnegap0  10498  expcllem  10501  mulexp  10529  expadd  10532  expaddzap  10534  expmulzap  10536  expdivap  10541  leexp1a  10545  expnlbnd  10614  bcpasc  10714  bccl  10715  hashfacen  10784  seq3coll  10790  seq3shft  10815  resqrexlemfp1  10986  sqrtdiv  11019  climshftlemg  11278  climcn1  11284  climsqz  11311  climsqz2  11312  clim2ser  11313  clim2ser2  11314  isermulc2  11316  climub  11320  serf0  11328  fsum3cvg  11354  sumrbdc  11355  summodclem3  11356  summodclem2a  11357  zsumdc  11360  fsumf1o  11366  isumss  11367  fisumss  11368  isumss2  11369  fsum3cvg2  11370  fsum3cvg3  11372  fsumcl2lem  11374  fsumcllem  11375  fsumadd  11382  fsumsplit  11383  fsumsplitsn  11386  sumsplitdc  11408  fisumrev2  11422  fsum2mul  11429  fsum00  11438  telfsumo  11442  fsumparts  11446  iserabs  11451  cvgratnnlemabsle  11503  cvgratnn  11507  cvgratz  11508  mertenslemub  11510  mertenslemi1  11511  mertenslem2  11512  mertensabs  11513  clim2prod  11515  clim2divap  11516  prodfap0  11521  prodfrecap  11522  prodeq2  11533  fproddccvg  11548  prodrbdclem2  11549  prodmodc  11554  zproddc  11555  fprodf1o  11564  fprodssdc  11566  fprodunsn  11580  fprodcllem  11582  fprodabs  11592  fprodeq0  11593  fprodmodd  11617  eftlcvg  11663  negdvdsb  11782  dvdsnegb  11783  dvdsext  11828  addmodlteqALT  11832  nno  11878  infssuzex  11917  zsupssdc  11922  gcdsupex  11925  gcdsupcl  11926  bezoutlembz  11972  dvdssq  11999  eucalgf  12022  dvdslcm  12036  lcmledvds  12037  lcmeq0  12038  lcmcl  12039  lcmdvds  12046  lcmgcdeq  12050  divgcdcoprmex  12069  isprm5lem  12108  phibndlem  12183  phiprmpw  12189  pc2dvds  12296  pcmpt  12308  prmpwdvds  12320  1arith  12332  ctiunctlemf  12406  ctiunct  12408  grprinvd  12671  grpridd  12672  mndpropd  12707  mhmpropd  12720  0mhm  12735  grplcan  12793  mulgval  12847  mulgnn0z  12870  mulgnndir  12872  mulgnn0dir  12873  srglmhm  12973  srgrmhm  12974  ringpropd  13013  crngpropd  13014  mulgass3  13049  opnssneib  13227  neissex  13236  tgrest  13240  iscnp3  13274  cnpnei  13290  cnrest  13306  tx1cn  13340  txcnp  13342  elbl3ps  13465  elbl3  13466  blininf  13495  blssexps  13500  blssex  13501  blpnfctr  13510  mopni2  13554  blsscls2  13564  metss  13565  bdmet  13573  metrest  13577  metcn  13585  txmetcn  13590  bl2ioo  13613  ivthinclemlr  13686  ivthinclemur  13688  dvcj  13744  dvfre  13745  coseq0q4123  13826  abssinper  13838  lgsval2lem  13982  lgsval4lem  13983  lgsneg  13996  lgsmod  13998  lgsdir2  14005  lgsdir  14007  lgsne0  14010  lgssq  14012  subctctexmid  14311  cvgcmp2n  14342  iswomninnlem  14358  nconstwlpo  14374