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  1186  3ad2antl2  1187  ad4ant124  1243  3adant1r  1258  ad5ant235  1265  ad5ant135  1270  bilukdc  1441  elpr2elpr  3880  intab  3978  pofun  4433  ralxfrd  4583  rexxfrd  4584  ordtri2or2exmidlem  4648  wessep  4700  poinxp  4819  relop  4905  fun11iun  5635  ssimaex  5738  fndmdif  5783  fconst2g  5899  foeqcnvco  5963  f1eqcocnv  5964  isocnv  5984  isocnv2  5985  riota2df  6025  caofdig  6300  f1o2ndf1  6424  tfr1onlembacc  6573  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllembacc  6586  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  tfrcl  6595  xpdom2  7082  fimax2gtrilemstep  7158  xpfi  7192  eqsupti  7287  ordiso2  7326  enumctlemm  7405  enwomnilem  7460  cc2lem  7580  mulcanpig  7650  prarloclemlt  7808  genpdf  7823  genpdisj  7838  addnqprl  7844  addnqpru  7845  addlocpr  7851  prmuloc  7881  mulnqprl  7883  mulnqpru  7884  mullocpr  7886  ltpopr  7910  ltsopr  7911  ltaddpr  7912  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  ltaprg  7934  recexprlemopu  7942  recexprlemloc  7946  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  suplocsrlem  8123  axcaucvglemcau  8213  axpre-suploclemres  8216  axsuploc  8346  cnegexlem1  8448  cnegexlem3  8450  cnegex  8451  addsubeq4  8488  rimul  8859  divcanap6  8993  ltmul12a  9134  lemul12b  9135  lbinf  9222  zrevaddcl  9628  nzadd  9630  zextle  9669  fzind  9693  uz11  9877  infregelbex  9930  qreccl  9974  qrevaddcl  9976  irradd  9978  xrlttr  10128  xrltso  10129  xaddass  10202  xleadd1a  10206  xlt2add  10213  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  divelunit  10335  uzsubsubfz  10381  fzaddel  10393  fzrev  10418  elfzmlbp  10466  infssuzex  10593  zsupssdc  10598  frec2uzrdg  10771  frecuzrdgtcl  10774  frecuzrdgsuc  10776  frecuzrdgdomlem  10779  frecuzrdgfunlem  10781  frecuzrdgsuctlem  10785  iseqovex  10820  seq3val  10822  seqf  10826  seq3clss  10833  seq3fveq2  10837  seq3feq2  10838  seq3feq  10842  seq3shft2  10843  ser3mono  10849  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seq3caopr2  10855  seqcaopr2g  10856  iseqf1olemab  10864  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1oleml  10878  seqf1oglem2a  10880  seqf1oglem2  10882  seq3id3  10886  seq3id  10887  seq3id2  10888  seq3homo  10889  seq3z  10890  seqfeq3  10891  seqhomog  10892  seqfeq4g  10893  ser3ge0  10898  expp1  10908  expnegap0  10909  expcllem  10912  mulexp  10940  expadd  10943  expaddzap  10945  expmulzap  10947  expdivap  10952  leexp1a  10956  expnlbnd  11026  bcpasc  11128  bccl  11129  hashfacen  11206  seq3coll  11212  ccatlen  11281  ccatvalfn  11287  ccatsymb  11288  ccatalpha  11299  pfxclz  11369  wrd2ind  11413  swrdccat  11425  seq3shft  11521  resqrexlemfp1  11692  sqrtdiv  11725  climshftlemg  11985  climcn1  11991  climsqz  12018  climsqz2  12019  clim2ser  12020  clim2ser2  12021  isermulc2  12023  climub  12027  serf0  12035  fsum3cvg  12062  sumrbdc  12063  summodclem3  12064  summodclem2a  12065  zsumdc  12068  fsumf1o  12074  isumss  12075  fisumss  12076  isumss2  12077  fsum3cvg2  12078  fsum3cvg3  12080  fsumcl2lem  12082  fsumcllem  12083  fsumadd  12090  fsumsplit  12091  fsumsplitsn  12094  sumsplitdc  12116  fisumrev2  12130  fsum2mul  12137  fsum00  12146  telfsumo  12150  fsumparts  12154  iserabs  12159  cvgratnnlemabsle  12211  cvgratnn  12215  cvgratz  12216  mertenslemub  12218  mertenslemi1  12219  mertenslem2  12220  mertensabs  12221  clim2prod  12223  clim2divap  12224  prodfap0  12229  prodfrecap  12230  prodeq2  12241  fproddccvg  12256  prodrbdclem2  12257  prodmodc  12262  zproddc  12263  fprodf1o  12272  fprodssdc  12274  fprodunsn  12288  fprodcllem  12290  fprodabs  12300  fprodeq0  12301  fprodmodd  12325  eftlcvg  12371  negdvdsb  12491  dvdsnegb  12492  fsumdvds  12526  dvdsext  12539  addmodlteqALT  12543  nno  12590  gcdsupex  12651  gcdsupcl  12652  bezoutlembz  12698  dvdssq  12725  eucalgf  12750  dvdslcm  12764  lcmledvds  12765  lcmeq0  12766  lcmcl  12767  lcmdvds  12774  lcmgcdeq  12778  divgcdcoprmex  12797  isprm5lem  12836  phibndlem  12911  phiprmpw  12917  pc2dvds  13026  pcmpt  13039  prmpwdvds  13051  1arith  13063  4sqleminfi  13093  ctiunctlemf  13187  ctiunct  13189  grpinva  13597  grprida  13598  gsumpropd2  13604  sgrppropd  13624  prdssgrpd  13626  mndpropd  13651  prdsidlem  13658  prdsmndd  13659  mhmpropd  13677  0mhm  13697  resmhm2  13699  resmhm2b  13700  grplcan  13773  mulgval  13837  mulgnn0z  13864  mulgnndir  13866  mulgnn0dir  13867  issubg2m  13904  issubg4m  13908  subgintm  13913  ghmf1  13988  gsumfzmptfidmadd  14054  gsumfzmhm  14058  srglmhm  14135  srgrmhm  14136  ringpropd  14180  crngpropd  14181  ringlghm  14203  ringrghm  14204  mulgass3  14227  issubrng2  14353  subrngpropd  14359  issubrg2  14384  subrgintm  14386  subrgpropd  14396  rhmpropd  14397  unitrrg  14411  lmodprop2d  14494  islss3  14525  lssintclm  14530  qusrhm  14674  gsumfzfsum  14734  opnssneib  15019  neissex  15028  tgrest  15032  iscnp3  15066  cnpnei  15082  cnrest  15098  tx1cn  15132  txcnp  15134  elbl3ps  15257  elbl3  15258  blininf  15287  blssexps  15292  blssex  15293  blpnfctr  15302  mopni2  15346  blsscls2  15356  metss  15357  bdmet  15365  metrest  15369  metcn  15377  txmetcn  15382  bl2ioo  15413  ivthinclemlr  15500  ivthinclemur  15502  dvcj  15572  dvfre  15573  elplyd  15604  plyaddlem1  15610  plymullem1  15611  plymullem  15613  plycolemc  15621  plycjlemc  15623  coseq0q4123  15697  abssinper  15709  fsumdvdsmul  15857  lgsval2lem  15881  lgsval4lem  15882  lgsneg  15895  lgsmod  15897  lgsdir2  15904  lgsdir  15906  lgsne0  15909  lgssq  15911  lgsquadlem1  15948  usgredg2vlem2  16216  clwwlkccat  16394  clwwlknonex2lem2  16431  subctctexmid  16772  cvgcmp2n  16815  iswomninnlem  16832  nconstwlpo  16850