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  1185  3ad2antl2  1186  ad4ant124  1242  3adant1r  1257  ad5ant235  1264  ad5ant135  1269  bilukdc  1440  elpr2elpr  3859  intab  3957  pofun  4409  ralxfrd  4559  rexxfrd  4560  ordtri2or2exmidlem  4624  wessep  4676  poinxp  4795  relop  4880  fun11iun  5604  ssimaex  5707  fndmdif  5752  fconst2g  5869  foeqcnvco  5931  f1eqcocnv  5932  isocnv  5952  isocnv2  5953  riota2df  5993  caofdig  6269  f1o2ndf1  6393  tfr1onlembacc  6508  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllembacc  6521  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  tfrcl  6530  xpdom2  7015  fimax2gtrilemstep  7090  xpfi  7124  eqsupti  7195  ordiso2  7234  enumctlemm  7313  enwomnilem  7368  cc2lem  7485  mulcanpig  7555  prarloclemlt  7713  genpdf  7728  genpdisj  7743  addnqprl  7749  addnqpru  7750  addlocpr  7756  prmuloc  7786  mulnqprl  7788  mulnqpru  7789  mullocpr  7791  ltpopr  7815  ltsopr  7816  ltaddpr  7817  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprg  7839  recexprlemopu  7847  recexprlemloc  7851  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  suplocsrlem  8028  axcaucvglemcau  8118  axpre-suploclemres  8121  axsuploc  8252  cnegexlem1  8354  cnegexlem3  8356  cnegex  8357  addsubeq4  8394  rimul  8765  divcanap6  8899  ltmul12a  9040  lemul12b  9041  lbinf  9128  zrevaddcl  9530  nzadd  9532  zextle  9571  fzind  9595  uz11  9779  infregelbex  9832  qreccl  9876  qrevaddcl  9878  irradd  9880  xrlttr  10030  xrltso  10031  xaddass  10104  xleadd1a  10108  xlt2add  10115  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  divelunit  10237  uzsubsubfz  10282  fzaddel  10294  fzrev  10319  elfzmlbp  10367  infssuzex  10494  zsupssdc  10499  frec2uzrdg  10672  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  iseqovex  10721  seq3val  10723  seqf  10727  seq3clss  10734  seq3fveq2  10738  seq3feq2  10739  seq3feq  10743  seq3shft2  10744  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seq3caopr2  10756  seqcaopr2g  10757  iseqf1olemab  10765  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1oleml  10779  seqf1oglem2a  10781  seqf1oglem2  10783  seq3id3  10787  seq3id  10788  seq3id2  10789  seq3homo  10790  seq3z  10791  seqfeq3  10792  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  expp1  10809  expnegap0  10810  expcllem  10813  mulexp  10841  expadd  10844  expaddzap  10846  expmulzap  10848  expdivap  10853  leexp1a  10857  expnlbnd  10927  bcpasc  11029  bccl  11030  hashfacen  11101  seq3coll  11107  ccatlen  11173  ccatvalfn  11179  ccatsymb  11180  ccatalpha  11191  pfxclz  11261  wrd2ind  11305  swrdccat  11317  seq3shft  11400  resqrexlemfp1  11571  sqrtdiv  11604  climshftlemg  11864  climcn1  11870  climsqz  11897  climsqz2  11898  clim2ser  11899  clim2ser2  11900  isermulc2  11902  climub  11906  serf0  11914  fsum3cvg  11941  sumrbdc  11942  summodclem3  11943  summodclem2a  11944  zsumdc  11947  fsumf1o  11953  isumss  11954  fisumss  11955  isumss2  11956  fsum3cvg2  11957  fsum3cvg3  11959  fsumcl2lem  11961  fsumcllem  11962  fsumadd  11969  fsumsplit  11970  fsumsplitsn  11973  sumsplitdc  11995  fisumrev2  12009  fsum2mul  12016  fsum00  12025  telfsumo  12029  fsumparts  12033  iserabs  12038  cvgratnnlemabsle  12090  cvgratnn  12094  cvgratz  12095  mertenslemub  12097  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  clim2prod  12102  clim2divap  12103  prodfap0  12108  prodfrecap  12109  prodeq2  12120  fproddccvg  12135  prodrbdclem2  12136  prodmodc  12141  zproddc  12142  fprodf1o  12151  fprodssdc  12153  fprodunsn  12167  fprodcllem  12169  fprodabs  12179  fprodeq0  12180  fprodmodd  12204  eftlcvg  12250  negdvdsb  12370  dvdsnegb  12371  fsumdvds  12405  dvdsext  12418  addmodlteqALT  12422  nno  12469  gcdsupex  12530  gcdsupcl  12531  bezoutlembz  12577  dvdssq  12604  eucalgf  12629  dvdslcm  12643  lcmledvds  12644  lcmeq0  12645  lcmcl  12646  lcmdvds  12653  lcmgcdeq  12657  divgcdcoprmex  12676  isprm5lem  12715  phibndlem  12790  phiprmpw  12796  pc2dvds  12905  pcmpt  12918  prmpwdvds  12930  1arith  12942  4sqleminfi  12972  ctiunctlemf  13061  ctiunct  13063  grpinva  13471  grprida  13472  gsumpropd2  13478  sgrppropd  13498  prdssgrpd  13500  mndpropd  13525  prdsidlem  13532  prdsmndd  13533  mhmpropd  13551  0mhm  13571  resmhm2  13573  resmhm2b  13574  grplcan  13647  mulgval  13711  mulgnn0z  13738  mulgnndir  13740  mulgnn0dir  13741  issubg2m  13778  issubg4m  13782  subgintm  13787  ghmf1  13862  gsumfzmptfidmadd  13928  gsumfzmhm  13932  srglmhm  14009  srgrmhm  14010  ringpropd  14054  crngpropd  14055  ringlghm  14077  ringrghm  14078  mulgass3  14101  issubrng2  14227  subrngpropd  14233  issubrg2  14258  subrgintm  14260  subrgpropd  14270  rhmpropd  14271  unitrrg  14284  lmodprop2d  14365  islss3  14396  lssintclm  14401  qusrhm  14545  gsumfzfsum  14605  opnssneib  14883  neissex  14892  tgrest  14896  iscnp3  14930  cnpnei  14946  cnrest  14962  tx1cn  14996  txcnp  14998  elbl3ps  15121  elbl3  15122  blininf  15151  blssexps  15156  blssex  15157  blpnfctr  15166  mopni2  15210  blsscls2  15220  metss  15221  bdmet  15229  metrest  15233  metcn  15241  txmetcn  15246  bl2ioo  15277  ivthinclemlr  15364  ivthinclemur  15366  dvcj  15436  dvfre  15437  elplyd  15468  plyaddlem1  15474  plymullem1  15475  plymullem  15477  plycolemc  15485  plycjlemc  15487  coseq0q4123  15561  abssinper  15573  fsumdvdsmul  15718  lgsval2lem  15742  lgsval4lem  15743  lgsneg  15756  lgsmod  15758  lgsdir2  15765  lgsdir  15767  lgsne0  15770  lgssq  15772  lgsquadlem1  15809  usgredg2vlem2  16077  clwwlkccat  16255  clwwlknonex2lem2  16292  subctctexmid  16622  cvgcmp2n  16658  iswomninnlem  16674  nconstwlpo  16691