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  6618  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllembacc  6631  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  tfrcl  6640  xpdom2  7135  fimax2gtrilemstep  7211  xpfi  7245  eqsupti  7342  ordiso2  7381  enumctlemm  7460  enwomnilem  7515  cc2lem  7638  mulcanpig  7708  prarloclemlt  7866  genpdf  7881  genpdisj  7896  addnqprl  7902  addnqpru  7903  addlocpr  7909  prmuloc  7939  mulnqprl  7941  mulnqpru  7942  mullocpr  7944  ltpopr  7968  ltsopr  7969  ltaddpr  7970  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltaprg  7992  recexprlemopu  8000  recexprlemloc  8004  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  suplocsrlem  8181  axcaucvglemcau  8271  axpre-suploclemres  8274  axsuploc  8404  cnegexlem1  8508  cnegexlem3  8510  cnegex  8511  addsubeq4  8548  rimul  8921  divcanap6  9057  ltmul12a  9198  lemul12b  9199  lbinf  9286  zrevaddcl  9704  nzadd  9706  zextle  9747  fzind  9771  uz11  9960  infregelbex  10013  qreccl  10057  qrevaddcl  10059  irradd  10061  xrlttr  10213  xrltso  10214  xaddass  10287  xleadd1a  10291  xlt2add  10298  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  divelunit  10420  uzsubsubfz  10468  fzaddel  10481  fzrev  10507  elfzmlbp  10555  infssuzex  10682  zsupssdc  10689  frec2uzrdg  10866  frecuzrdgtcl  10869  frecuzrdgsuc  10871  frecuzrdgdomlem  10874  frecuzrdgfunlem  10876  frecuzrdgsuctlem  10880  iseqovex  10915  seq3val  10917  seqf  10921  seq3clss  10928  seq3fveq2  10932  seq3feq2  10933  seq3feq  10937  seq3shft2  10938  ser3mono  10944  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemab  10959  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1oleml  10973  seqf1oglem2a  10975  seqf1oglem2  10977  seq3id3  10981  seq3id  10982  seq3id2  10983  seq3homo  10984  seq3z  10985  seqfeq3  10986  seqhomog  10987  seqfeq4g  10988  ser3ge0  10993  expp1  11003  expnegap0  11004  expcllem  11007  mulexp  11035  expadd  11038  expaddzap  11040  expmulzap  11042  expdivap  11047  leexp1a  11051  expnlbnd  11122  bcpasc  11225  bccl  11226  hashfacen  11305  seq3coll  11315  ccatlen  11384  ccatvalfn  11390  ccatsymb  11391  ccatalpha  11402  pfxclz  11472  wrd2ind  11516  swrdccat  11528  seq3shft  11624  resqrexlemfp1  11796  sqrtdiv  11829  climshftlemg  12092  climcn1  12098  climsqz  12125  climsqz2  12126  clim2ser  12127  clim2ser2  12128  isermulc2  12130  climub  12134  serf0  12142  fsum3cvg  12169  sumrbdc  12170  summodclem3  12171  summodclem2a  12172  zsumdc  12175  fsumf1o  12181  isumss  12182  fisumss  12183  isumss2  12184  fsum3cvg2  12185  fsum3cvg3  12187  fsumcl2lem  12189  fsumcllem  12190  fsumadd  12197  fsumsplit  12198  fsumsplitsn  12201  sumsplitdc  12223  fisumrev2  12237  fsum2mul  12244  fsum00  12253  telfsumo  12257  fsumparts  12261  iserabs  12266  cvgratnnlemabsle  12318  cvgratnn  12322  cvgratz  12323  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  clim2prod  12330  clim2divap  12331  prodfap0  12336  prodfrecap  12337  prodeq2  12348  fproddccvg  12363  prodrbdclem2  12364  prodmodc  12369  zproddc  12370  fprodf1o  12379  fprodssdc  12381  fprodunsn  12395  fprodcllem  12397  fprodabs  12407  fprodeq0  12408  fprodmodd  12432  eftlcvg  12478  negdvdsb  12598  dvdsnegb  12599  fsumdvds  12633  dvdsext  12646  addmodlteqALT  12650  nno  12697  gcdsupex  12758  gcdsupcl  12759  bezoutlembz  12805  dvdssq  12832  eucalgf  12857  dvdslcm  12871  lcmledvds  12872  lcmeq0  12873  lcmcl  12874  lcmdvds  12881  lcmgcdeq  12885  divgcdcoprmex  12904  isprm5lem  12944  phibndlem  13022  phiprmpw  13028  pc2dvds  13137  pcmpt  13150  prmpwdvds  13162  1arith  13174  4sqleminfi  13204  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsv  13310  ballotfilemsima  13316  ctiunctlemf  13386  ctiunct  13388  grpinva  13764  grprida  13765  sgrppropd  13786  mndpropd  13811  mhmpropd  13831  0mhm  13851  resmhm2  13853  resmhm2b  13854  grplcan  13925  mulgval  13983  mulgnn0z  14010  mulgnndir  14012  mulgnn0dir  14013  issubg2m  14050  issubg4m  14054  subgintm  14059  ghmf1  14134  resscntz  14165  cntzsgrpcl  14166  cntzsubm  14169  gzsummhm  14234  gsummptfidmsplit  14253  gsumressfi  14266  prdssgrpd  14297  prdsidlem  14299  prdsmndd  14300  srglmhm  14403  srgrmhm  14404  ringpropd  14449  crngpropd  14450  ringlghm  14472  ringrghm  14473  mulgass3  14499  issubrng2  14626  subrngpropd  14632  issubrg2  14657  subrgintm  14659  subrgpropd  14669  rhmpropd  14670  unitrrg  14684  lmodprop2d  14793  islss3  14824  lssintclm  14829  qusrhm  14973  issubassa3  15120  opnssneib  15399  neissex  15408  tgrest  15412  iscnp3  15446  cnpnei  15462  cnrest  15478  tx1cn  15512  txcnp  15514  elbl3ps  15637  elbl3  15638  blininf  15667  blssexps  15672  blssex  15673  blpnfctr  15682  mopni2  15726  blsscls2  15736  metss  15737  bdmet  15745  metrest  15749  metcn  15757  txmetcn  15762  bl2ioo  15793  ivthinclemlr  15880  ivthinclemur  15882  dvcj  15952  dvfre  15953  elplyd  15984  plyaddlem1  15990  plymullem1  15991  plymullem  15993  plycolemc  16001  plycjlemc  16003  coseq0q4123  16078  abssinper  16090  fsumdvdsmul  16302  ppiqub  16310  bposlem5  16332  lgsval2lem  16351  lgsval4lem  16352  lgsneg  16365  lgsmod  16367  lgsdir2  16374  lgsdir  16376  lgsne0  16379  lgssq  16381  lgsquadlem1  16418  usgredg2vlem2  16686  clwwlkccat  16864  clwwlknonex2lem2  16901  subctctexmid  17252  cvgcmp2n  17305  iswomninnlem  17323  nconstwlpo  17340