Theorem adantlr 481

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 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2antrr  492  ad2ant2r  513  ad2ant2rl  515  adantl3r  516  ad4ant14  518  ad4ant24  520  ad5ant13  523  ad5ant14  524  ad5ant15  525  3ad2antl1  1190  3ad2antl2  1191  ad4ant124  1247  3adant1r  1262  ad5ant235  1269  ad5ant135  1274  bilukdc  1445  ifeqeqxdc  3687  elpr2elpr  3901  intab  3999  pofun  4459  ralxfrd  4610  rexxfrd  4611  ordtri2or2exmidlem  4675  wessep  4727  poinxp  4846  relop  4932  fun11iun  5663  relndmfv  5731  ssimaex  5767  fndmdif  5817  fconst2g  5933  foeqcnvco  5999  f1eqcocnv  6000  isocnv  6020  isocnv2  6021  riota2df  6063  caofdig  6340  f1o2ndf1  6468  tfr1onlembacc  6617  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllembacc  6630  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  tfrcl  6639  xpdom2  7134  fimax2gtrilemstep  7210  xpfi  7244  eqsupti  7343  ordiso2  7382  enumctlemm  7461  enwomnilem  7516  cc2lem  7639  mulcanpig  7709  prarloclemlt  7867  genpdf  7882  genpdisj  7897  addnqprl  7903  addnqpru  7904  addlocpr  7910  prmuloc  7940  mulnqprl  7942  mulnqpru  7943  mullocpr  7945  ltpopr  7969  ltsopr  7970  ltaddpr  7971  ltexprlemdisj  7980  ltexprlemloc  7981  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  ltaprg  7993  recexprlemopu  8001  recexprlemloc  8005  cauappcvgprlemladdfl  8029  cauappcvgprlemladdru  8030  caucvgsrlemcau  8167  caucvgsrlemgt1  8169  caucvgsrlemoffcau  8172  caucvgsrlemoffres  8174  suplocsrlem  8182  axcaucvglemcau  8272  axpre-suploclemres  8275  axsuploc  8405  cnegexlem1  8509  cnegexlem3  8511  cnegex  8512  addsubeq4  8549  rimul  8922  divcanap6  9058  ltmul12a  9199  lemul12b  9200  lbinf  9287  zrevaddcl  9707  nzadd  9709  zextle  9749  fzind  9773  uz11  9962  infregelbex  10015  qreccl  10059  qrevaddcl  10061  irradd  10063  xrlttr  10215  xrltso  10216  xaddass  10289  xleadd1a  10293  xlt2add  10300  iccshftr  10414  iccshftl  10416  iccdil  10418  icccntr  10420  divelunit  10422  uzsubsubfz  10470  fzaddel  10483  fzrev  10509  elfzmlbp  10557  infssuzex  10684  zsupssdc  10691  frec2uzrdg  10868  frecuzrdgtcl  10871  frecuzrdgsuc  10873  frecuzrdgdomlem  10876  frecuzrdgfunlem  10878  frecuzrdgsuctlem  10882  iseqovex  10917  seq3val  10919  seqf  10923  seq3clss  10930  seq3fveq2  10934  seq3feq2  10935  seq3feq  10939  seq3shft2  10940  ser3mono  10946  seq3split  10947  seqsplitg  10948  seq3caopr3  10950  seq3caopr2  10952  seqcaopr2g  10953  iseqf1olemab  10961  seq3f1olemqsumkj  10970  seq3f1olemqsumk  10971  seq3f1olemqsum  10972  seq3f1olemstep  10973  seq3f1oleml  10975  seqf1oglem2a  10977  seqf1oglem2  10979  seq3id3  10983  seq3id  10984  seq3id2  10985  seq3homo  10986  seq3z  10987  seqfeq3  10988  seqhomog  10989  seqfeq4g  10990  ser3ge0  10995  expp1  11005  expnegap0  11006  expcllem  11009  mulexp  11037  expadd  11040  expaddzap  11042  expmulzap  11044  expdivap  11049  leexp1a  11053  expnlbnd  11124  bcpasc  11227  bccl  11228  hashfacen  11307  seq3coll  11317  ccatlen  11386  ccatvalfn  11392  ccatsymb  11393  ccatalpha  11404  pfxclz  11474  wrd2ind  11518  swrdccat  11530  seq3shft  11626  resqrexlemfp1  11798  sqrtdiv  11831  climshftlemg  12094  climcn1  12100  climsqz  12127  climsqz2  12128  clim2ser  12129  clim2ser2  12130  isermulc2  12132  climub  12136  serf0  12144  fsum3cvg  12171  sumrbdc  12172  summodclem3  12173  summodclem2a  12174  zsumdc  12177  fsumf1o  12183  isumss  12184  fisumss  12185  isumss2  12186  fsum3cvg2  12187  fsum3cvg3  12189  fsumcl2lem  12191  fsumcllem  12192  fsumadd  12199  fsumsplit  12200  fsumsplitsn  12203  sumsplitdc  12225  fisumrev2  12239  fsum2mul  12246  fsum00  12255  telfsumo  12259  fsumparts  12263  iserabs  12268  cvgratnnlemabsle  12320  cvgratnn  12324  cvgratz  12325  mertenslemub  12327  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  clim2prod  12332  clim2divap  12333  prodfap0  12338  prodfrecap  12339  prodeq2  12350  fproddccvg  12365  prodrbdclem2  12366  prodmodc  12371  zproddc  12372  fprodf1o  12381  fprodssdc  12383  fprodunsn  12397  fprodcllem  12399  fprodabs  12409  fprodeq0  12410  fprodmodd  12434  eftlcvg  12480  negdvdsb  12600  dvdsnegb  12601  fsumdvds  12635  dvdsext  12648  addmodlteqALT  12652  nno  12699  gcdsupex  12760  gcdsupcl  12761  bezoutlembz  12807  dvdssq  12834  eucalgf  12859  dvdslcm  12873  lcmledvds  12874  lcmeq0  12875  lcmcl  12876  lcmdvds  12883  lcmgcdeq  12887  divgcdcoprmex  12906  isprm5lem  12946  phibndlem  13024  phiprmpw  13030  pc2dvds  13139  pcmpt  13152  prmpwdvds  13164  1arith  13176  4sqleminfi  13206  ballotfilemic  13309  ballotfilem1c  13310  ballotfilemsv  13312  ballotfilemsima  13318  ctiunctlemf  13388  ctiunct  13390  grpinva  13766  grprida  13767  sgrppropd  13788  mndpropd  13813  mhmpropd  13833  0mhm  13853  resmhm2  13855  resmhm2b  13856  grplcan  13927  mulgval  13985  mulgnn0z  14012  mulgnndir  14014  mulgnn0dir  14015  issubg2m  14052  issubg4m  14056  subgintm  14061  ghmf1  14136  resscntz  14167  cntzsgrpcl  14168  cntzsubm  14171  gzsummhm  14236  gsummptfidmsplit  14255  gsumressfi  14268  prdssgrpd  14299  prdsidlem  14301  prdsmndd  14302  srglmhm  14405  srgrmhm  14406  ringpropd  14451  crngpropd  14452  ringlghm  14474  ringrghm  14475  mulgass3  14501  issubrng2  14628  subrngpropd  14634  issubrg2  14659  subrgintm  14661  subrgpropd  14671  rhmpropd  14672  unitrrg  14686  lmodprop2d  14795  islss3  14826  lssintclm  14831  qusrhm  14975  issubassa3  15122  opnssneib  15394  neissex  15403  tgrest  15407  iscnp3  15441  cnpnei  15457  cnrest  15473  tx1cn  15507  txcnp  15509  elbl3ps  15632  elbl3  15633  blininf  15662  blssexps  15667  blssex  15668  blpnfctr  15677  mopni2  15721  blsscls2  15731  metss  15732  bdmet  15740  metrest  15744  metcn  15752  txmetcn  15757  bl2ioo  15788  ivthinclemlr  15875  ivthinclemur  15877  dvcj  15947  dvfre  15948  elplyd  15979  plyaddlem1  15985  plymullem1  15986  plymullem  15988  plycolemc  15996  plycjlemc  15998  coseq0q4123  16073  abssinper  16085  fsumdvdsmul  16297  ppiqub  16305  bposlem5  16327  lgsval2lem  16346  lgsval4lem  16347  lgsneg  16360  lgsmod  16362  lgsdir2  16369  lgsdir  16371  lgsne0  16374  lgssq  16376  lgsquadlem1  16413  usgredg2vlem2  16681  clwwlkccat  16859  clwwlknonex2lem2  16896  subctctexmid  17247  cvgcmp2n  17300  iswomninnlem  17318  nconstwlpo  17335