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  1161  3ad2antl2  1162  ad4ant124  1218  3adant1r  1233  ad5ant235  1240  ad5ant135  1245  bilukdc  1407  intab  3888  pofun  4330  ralxfrd  4480  rexxfrd  4481  ordtri2or2exmidlem  4543  wessep  4595  poinxp  4713  relop  4795  fun11iun  5501  ssimaex  5598  fndmdif  5642  fconst2g  5752  foeqcnvco  5812  f1eqcocnv  5813  isocnv  5833  isocnv2  5834  riota2df  5873  f1o2ndf1  6254  tfr1onlembacc  6368  tfr1onlemaccex  6374  tfr1onlemres  6375  tfrcllembacc  6381  tfrcllemaccex  6387  tfrcllemres  6388  tfrcldm  6389  tfrcl  6390  xpdom2  6858  fimax2gtrilemstep  6929  xpfi  6959  eqsupti  7026  ordiso2  7065  enumctlemm  7144  enwomnilem  7198  cc2lem  7296  mulcanpig  7365  prarloclemlt  7523  genpdf  7538  genpdisj  7553  addnqprl  7559  addnqpru  7560  addlocpr  7566  prmuloc  7596  mulnqprl  7598  mulnqpru  7599  mullocpr  7601  ltpopr  7625  ltsopr  7626  ltaddpr  7627  ltexprlemdisj  7636  ltexprlemloc  7637  ltexprlemru  7642  addcanprleml  7644  addcanprlemu  7645  ltaprg  7649  recexprlemopu  7657  recexprlemloc  7661  cauappcvgprlemladdfl  7685  cauappcvgprlemladdru  7686  caucvgsrlemcau  7823  caucvgsrlemgt1  7825  caucvgsrlemoffcau  7828  caucvgsrlemoffres  7830  suplocsrlem  7838  axcaucvglemcau  7928  axpre-suploclemres  7931  axsuploc  8061  cnegexlem1  8163  cnegexlem3  8165  cnegex  8166  addsubeq4  8203  rimul  8573  divcanap6  8707  ltmul12a  8848  lemul12b  8849  lbinf  8936  zrevaddcl  9334  nzadd  9336  zextle  9375  fzind  9399  uz11  9582  infregelbex  9630  qreccl  9674  qrevaddcl  9676  irradd  9678  xrlttr  9827  xrltso  9828  xaddass  9901  xleadd1a  9905  xlt2add  9912  iccshftr  10026  iccshftl  10028  iccdil  10030  icccntr  10032  divelunit  10034  uzsubsubfz  10079  fzaddel  10091  fzrev  10116  elfzmlbp  10164  frec2uzrdg  10442  frecuzrdgtcl  10445  frecuzrdgsuc  10447  frecuzrdgdomlem  10450  frecuzrdgfunlem  10452  frecuzrdgsuctlem  10456  iseqovex  10489  seq3val  10491  seqf  10494  seq3clss  10500  seq3fveq2  10502  seq3feq2  10503  seq3feq  10505  seq3shft2  10506  ser3mono  10511  seq3split  10512  seq3caopr3  10514  seq3caopr2  10515  iseqf1olemab  10522  seq3f1olemqsumkj  10531  seq3f1olemqsumk  10532  seq3f1olemqsum  10533  seq3f1olemstep  10534  seq3f1oleml  10536  seq3id3  10540  seq3id  10541  seq3id2  10542  seq3homo  10543  seq3z  10544  seqfeq3  10545  seqfeq4g  10546  ser3ge0  10551  expp1  10561  expnegap0  10562  expcllem  10565  mulexp  10593  expadd  10596  expaddzap  10598  expmulzap  10600  expdivap  10605  leexp1a  10609  expnlbnd  10679  bcpasc  10781  bccl  10782  hashfacen  10851  seq3coll  10857  seq3shft  10882  resqrexlemfp1  11053  sqrtdiv  11086  climshftlemg  11345  climcn1  11351  climsqz  11378  climsqz2  11379  clim2ser  11380  clim2ser2  11381  isermulc2  11383  climub  11387  serf0  11395  fsum3cvg  11421  sumrbdc  11422  summodclem3  11423  summodclem2a  11424  zsumdc  11427  fsumf1o  11433  isumss  11434  fisumss  11435  isumss2  11436  fsum3cvg2  11437  fsum3cvg3  11439  fsumcl2lem  11441  fsumcllem  11442  fsumadd  11449  fsumsplit  11450  fsumsplitsn  11453  sumsplitdc  11475  fisumrev2  11489  fsum2mul  11496  fsum00  11505  telfsumo  11509  fsumparts  11513  iserabs  11518  cvgratnnlemabsle  11570  cvgratnn  11574  cvgratz  11575  mertenslemub  11577  mertenslemi1  11578  mertenslem2  11579  mertensabs  11580  clim2prod  11582  clim2divap  11583  prodfap0  11588  prodfrecap  11589  prodeq2  11600  fproddccvg  11615  prodrbdclem2  11616  prodmodc  11621  zproddc  11622  fprodf1o  11631  fprodssdc  11633  fprodunsn  11647  fprodcllem  11649  fprodabs  11659  fprodeq0  11660  fprodmodd  11684  eftlcvg  11730  negdvdsb  11849  dvdsnegb  11850  dvdsext  11896  addmodlteqALT  11900  nno  11946  infssuzex  11985  zsupssdc  11990  gcdsupex  11993  gcdsupcl  11994  bezoutlembz  12040  dvdssq  12067  eucalgf  12090  dvdslcm  12104  lcmledvds  12105  lcmeq0  12106  lcmcl  12107  lcmdvds  12114  lcmgcdeq  12118  divgcdcoprmex  12137  isprm5lem  12176  phibndlem  12251  phiprmpw  12257  pc2dvds  12365  pcmpt  12378  prmpwdvds  12390  1arith  12402  4sqleminfi  12432  ctiunctlemf  12492  ctiunct  12494  grpinva  12865  grprida  12866  gsumpropd2  12871  sgrppropd  12891  mndpropd  12916  mhmpropd  12933  0mhm  12953  resmhm2  12955  resmhm2b  12956  grplcan  13021  mulgval  13079  mulgnn0z  13106  mulgnndir  13108  mulgnn0dir  13109  issubg2m  13145  issubg4m  13149  subgintm  13154  ghmf1  13229  srglmhm  13364  srgrmhm  13365  ringpropd  13409  crngpropd  13410  mulgass3  13452  issubrng2  13574  subrngpropd  13580  issubrg2  13605  subrgintm  13607  subrgpropd  13612  lmodprop2d  13681  islss3  13712  lssintclm  13717  opnssneib  14133  neissex  14142  tgrest  14146  iscnp3  14180  cnpnei  14196  cnrest  14212  tx1cn  14246  txcnp  14248  elbl3ps  14371  elbl3  14372  blininf  14401  blssexps  14406  blssex  14407  blpnfctr  14416  mopni2  14460  blsscls2  14470  metss  14471  bdmet  14479  metrest  14483  metcn  14491  txmetcn  14496  bl2ioo  14519  ivthinclemlr  14592  ivthinclemur  14594  dvcj  14650  dvfre  14651  coseq0q4123  14732  abssinper  14744  lgsval2lem  14889  lgsval4lem  14890  lgsneg  14903  lgsmod  14905  lgsdir2  14912  lgsdir  14914  lgsne0  14917  lgssq  14919  subctctexmid  15229  cvgcmp2n  15260  iswomninnlem  15276  nconstwlpo  15293