Theorem adantlr 460

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 107	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 277	1 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  ad2antrr  471  ad2ant2r  492  ad2ant2rl  494  3ad2antl1  1100  3ad2antl2  1101  3adant1r  1162  bilukdc  1327  intab  3665  pofun  4067  ralxfrd  4212  rexxfrd  4213  ordtri2or2exmidlem  4269  wessep  4320  poinxp  4427  relop  4504  fun11iun  5167  ssimaex  5255  fndmdif  5293  fconst2g  5397  foeqcnvco  5450  f1eqcocnv  5451  isocnv  5471  isocnv2  5472  riota2df  5508  grprinvd  5716  grpridd  5717  f1o2ndf1  5869  xpdom2  6328  eqsupti  6409  ordiso2  6446  mulcanpig  6525  prarloclemlt  6683  genpdf  6698  genpdisj  6713  addnqprl  6719  addnqpru  6720  addlocpr  6726  prmuloc  6756  mulnqprl  6758  mulnqpru  6759  mullocpr  6761  ltpopr  6785  ltsopr  6786  ltaddpr  6787  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  ltaprg  6809  recexprlemopu  6817  recexprlemloc  6821  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  axcaucvglemcau  7064  cnegexlem1  7283  cnegexlem3  7285  cnegex  7286  addsubeq4  7323  rimul  7685  divcanap6  7807  ltmul12a  7938  lemul12b  7939  lbinf  8026  zrevaddcl  8401  nzadd  8403  zextle  8438  fzind  8462  uz11  8641  qreccl  8727  qrevaddcl  8729  irradd  8731  xrlttr  8870  xrltso  8871  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  divelunit  9024  uzsubsubfz  9066  fzaddel  9077  fzrev  9101  elfzmlbp  9143  frec2uzrdg  9411  frecuzrdgfn  9414  frecuzrdgcl  9415  frecuzrdgsuc  9417  iseqovex  9439  iseqval  9440  iseqf  9444  iseqss  9446  iseqfveq2  9448  iseqfeq2  9449  iseqfeq  9451  iseqshft2  9452  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqid3s  9466  iseqid  9467  iseqhomo  9468  iseqz  9469  expivallem  9477  expival  9478  expp1  9483  expnegap0  9484  expcllem  9487  mulexp  9515  expadd  9518  expaddzap  9520  expmulzap  9522  expdivap  9527  leexp1a  9531  expnlbnd  9597  bcpasc  9693  bccl  9694  resqrexlemfp1  9895  sqrtdiv  9928  climshftlemg  10141  climcn1  10147  climsqz  10173  climsqz2  10174  clim2iser  10175  clim2iser2  10176  iisermulc2  10178  iserile  10180  climub  10182  climserile  10183  serif0  10189  negdvdsb  10211  dvdsnegb  10212  dvdsext  10255  addmodlteqALT  10259  nno  10306  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  bezoutlembz  10393  dvdssq  10420  eucalgf  10437  dvdslcm  10451  lcmledvds  10452  lcmeq0  10453  lcmcl  10454  lcmdvds  10461  lcmgcdeq  10465  divgcdcoprmex  10484