Theorem adantlr 461

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  472  ad2ant2r  493  ad2ant2rl  495  3ad2antl1  1103  3ad2antl2  1104  3adant1r  1165  bilukdc  1330  intab  3700  pofun  4113  ralxfrd  4258  rexxfrd  4259  ordtri2or2exmidlem  4315  wessep  4366  poinxp  4475  relop  4554  fun11iun  5237  ssimaex  5328  fndmdif  5367  fconst2g  5473  foeqcnvco  5530  f1eqcocnv  5531  isocnv  5551  isocnv2  5552  riota2df  5589  grprinvd  5797  grpridd  5798  f1o2ndf1  5950  tfr1onlembacc  6061  tfr1onlemaccex  6067  tfr1onlemres  6068  tfrcllembacc  6074  tfrcllemaccex  6080  tfrcllemres  6081  tfrcldm  6082  tfrcl  6083  xpdom2  6499  fimax2gtrilemstep  6568  xpfi  6590  eqsupti  6635  ordiso2  6672  mulcanpig  6838  prarloclemlt  6996  genpdf  7011  genpdisj  7026  addnqprl  7032  addnqpru  7033  addlocpr  7039  prmuloc  7069  mulnqprl  7071  mulnqpru  7072  mullocpr  7074  ltpopr  7098  ltsopr  7099  ltaddpr  7100  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  ltaprg  7122  recexprlemopu  7130  recexprlemloc  7134  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  caucvgsrlemcau  7282  caucvgsrlemgt1  7284  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  axcaucvglemcau  7377  cnegexlem1  7601  cnegexlem3  7603  cnegex  7604  addsubeq4  7641  rimul  8003  divcanap6  8125  ltmul12a  8256  lemul12b  8257  lbinf  8344  zrevaddcl  8733  nzadd  8735  zextle  8770  fzind  8794  uz11  8973  qreccl  9059  qrevaddcl  9061  irradd  9063  xrlttr  9197  xrltso  9198  iccshftr  9343  iccshftl  9345  iccdil  9347  icccntr  9349  divelunit  9351  uzsubsubfz  9393  fzaddel  9404  fzrev  9428  elfzmlbp  9471  frec2uzrdg  9744  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgdomlem  9752  frecuzrdgfunlem  9754  frecuzrdgsuctlem  9758  iseqovex  9787  iseqval  9788  iseqvalt  9790  iseqfclt  9794  iseqoveq  9798  iseqss  9799  iseqsst  9800  iseqfveq2  9802  iseqfeq2  9803  iseqfeq  9805  iseqshft2  9806  isermono  9811  iseqsplit  9812  iseqcaopr3  9814  iseqcaopr2  9815  iseqf1olemab  9822  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1olemstep  9834  iseqf1oleml  9836  iseqid3s  9841  iseqid  9842  iseqid2  9843  iseqhomo  9844  iseqz  9845  expivallem  9854  expival  9855  expp1  9860  expnegap0  9861  expcllem  9864  mulexp  9892  expadd  9895  expaddzap  9897  expmulzap  9899  expdivap  9904  leexp1a  9908  expnlbnd  9974  bcpasc  10070  bccl  10071  hashfacen  10137  iseqcoll  10143  resqrexlemfp1  10337  sqrtdiv  10370  climshftlemg  10583  climcn1  10589  climsqz  10615  climsqz2  10616  clim2iser  10617  clim2iser2  10618  iisermulc2  10620  iserile  10622  climub  10624  climserile  10625  serif0  10631  fisumcvg  10656  isumrb  10657  isummolem3  10659  isummolem2a  10660  zisum  10663  fsumf1o  10668  isumss  10669  fisumss  10670  negdvdsb  10687  dvdsnegb  10688  dvdsext  10731  addmodlteqALT  10735  nno  10781  infssuzex  10820  gcdsupex  10824  gcdsupcl  10825  bezoutlembz  10868  dvdssq  10895  eucalgf  10912  dvdslcm  10926  lcmledvds  10927  lcmeq0  10928  lcmcl  10929  lcmdvds  10936  lcmgcdeq  10940  divgcdcoprmex  10959  phibndlem  11067  phiprmpw  11073