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  1186  3ad2antl2  1187  ad4ant124  1243  3adant1r  1258  ad5ant235  1265  ad5ant135  1270  bilukdc  1441  elpr2elpr  3882  intab  3980  pofun  4435  ralxfrd  4585  rexxfrd  4586  ordtri2or2exmidlem  4650  wessep  4702  poinxp  4821  relop  4907  fun11iun  5637  ssimaex  5740  fndmdif  5785  fconst2g  5901  foeqcnvco  5965  f1eqcocnv  5966  isocnv  5986  isocnv2  5987  riota2df  6027  caofdig  6302  f1o2ndf1  6426  tfr1onlembacc  6575  tfr1onlemaccex  6581  tfr1onlemres  6582  tfrcllembacc  6588  tfrcllemaccex  6594  tfrcllemres  6595  tfrcldm  6596  tfrcl  6597  xpdom2  7084  fimax2gtrilemstep  7160  xpfi  7194  eqsupti  7289  ordiso2  7328  enumctlemm  7407  enwomnilem  7462  cc2lem  7585  mulcanpig  7655  prarloclemlt  7813  genpdf  7828  genpdisj  7843  addnqprl  7849  addnqpru  7850  addlocpr  7856  prmuloc  7886  mulnqprl  7888  mulnqpru  7889  mullocpr  7891  ltpopr  7915  ltsopr  7916  ltaddpr  7917  ltexprlemdisj  7926  ltexprlemloc  7927  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  ltaprg  7939  recexprlemopu  7947  recexprlemloc  7951  cauappcvgprlemladdfl  7975  cauappcvgprlemladdru  7976  caucvgsrlemcau  8113  caucvgsrlemgt1  8115  caucvgsrlemoffcau  8118  caucvgsrlemoffres  8120  suplocsrlem  8128  axcaucvglemcau  8218  axpre-suploclemres  8221  axsuploc  8351  cnegexlem1  8453  cnegexlem3  8455  cnegex  8456  addsubeq4  8493  rimul  8864  divcanap6  8998  ltmul12a  9139  lemul12b  9140  lbinf  9227  zrevaddcl  9633  nzadd  9635  zextle  9675  fzind  9699  uz11  9883  infregelbex  9936  qreccl  9980  qrevaddcl  9982  irradd  9984  xrlttr  10134  xrltso  10135  xaddass  10208  xleadd1a  10212  xlt2add  10219  iccshftr  10333  iccshftl  10335  iccdil  10337  icccntr  10339  divelunit  10341  uzsubsubfz  10387  fzaddel  10399  fzrev  10425  elfzmlbp  10473  infssuzex  10600  zsupssdc  10605  frec2uzrdg  10778  frecuzrdgtcl  10781  frecuzrdgsuc  10783  frecuzrdgdomlem  10786  frecuzrdgfunlem  10788  frecuzrdgsuctlem  10792  iseqovex  10827  seq3val  10829  seqf  10833  seq3clss  10840  seq3fveq2  10844  seq3feq2  10845  seq3feq  10849  seq3shft2  10850  ser3mono  10856  seq3split  10857  seqsplitg  10858  seq3caopr3  10860  seq3caopr2  10862  seqcaopr2g  10863  iseqf1olemab  10871  seq3f1olemqsumkj  10880  seq3f1olemqsumk  10881  seq3f1olemqsum  10882  seq3f1olemstep  10883  seq3f1oleml  10885  seqf1oglem2a  10887  seqf1oglem2  10889  seq3id3  10893  seq3id  10894  seq3id2  10895  seq3homo  10896  seq3z  10897  seqfeq3  10898  seqhomog  10899  seqfeq4g  10900  ser3ge0  10905  expp1  10915  expnegap0  10916  expcllem  10919  mulexp  10947  expadd  10950  expaddzap  10952  expmulzap  10954  expdivap  10959  leexp1a  10963  expnlbnd  11034  bcpasc  11136  bccl  11137  hashfacen  11216  seq3coll  11222  ccatlen  11291  ccatvalfn  11297  ccatsymb  11298  ccatalpha  11309  pfxclz  11379  wrd2ind  11423  swrdccat  11435  seq3shft  11531  resqrexlemfp1  11702  sqrtdiv  11735  climshftlemg  11995  climcn1  12001  climsqz  12028  climsqz2  12029  clim2ser  12030  clim2ser2  12031  isermulc2  12033  climub  12037  serf0  12045  fsum3cvg  12072  sumrbdc  12073  summodclem3  12074  summodclem2a  12075  zsumdc  12078  fsumf1o  12084  isumss  12085  fisumss  12086  isumss2  12087  fsum3cvg2  12088  fsum3cvg3  12090  fsumcl2lem  12092  fsumcllem  12093  fsumadd  12100  fsumsplit  12101  fsumsplitsn  12104  sumsplitdc  12126  fisumrev2  12140  fsum2mul  12147  fsum00  12156  telfsumo  12160  fsumparts  12164  iserabs  12169  cvgratnnlemabsle  12221  cvgratnn  12225  cvgratz  12226  mertenslemub  12228  mertenslemi1  12229  mertenslem2  12230  mertensabs  12231  clim2prod  12233  clim2divap  12234  prodfap0  12239  prodfrecap  12240  prodeq2  12251  fproddccvg  12266  prodrbdclem2  12267  prodmodc  12272  zproddc  12273  fprodf1o  12282  fprodssdc  12284  fprodunsn  12298  fprodcllem  12300  fprodabs  12310  fprodeq0  12311  fprodmodd  12335  eftlcvg  12381  negdvdsb  12501  dvdsnegb  12502  fsumdvds  12536  dvdsext  12549  addmodlteqALT  12553  nno  12600  gcdsupex  12661  gcdsupcl  12662  bezoutlembz  12708  dvdssq  12735  eucalgf  12760  dvdslcm  12774  lcmledvds  12775  lcmeq0  12776  lcmcl  12777  lcmdvds  12784  lcmgcdeq  12788  divgcdcoprmex  12807  isprm5lem  12846  phibndlem  12921  phiprmpw  12927  pc2dvds  13036  pcmpt  13049  prmpwdvds  13061  1arith  13073  4sqleminfi  13103  ctiunctlemf  13210  ctiunct  13212  grpinva  13620  grprida  13621  gsumpropd2  13627  sgrppropd  13647  prdssgrpd  13649  mndpropd  13674  prdsidlem  13681  prdsmndd  13682  mhmpropd  13700  0mhm  13720  resmhm2  13722  resmhm2b  13723  grplcan  13796  mulgval  13860  mulgnn0z  13887  mulgnndir  13889  mulgnn0dir  13890  issubg2m  13927  issubg4m  13931  subgintm  13936  ghmf1  14011  gsumfzmptfidmadd  14077  gsumfzmhm  14081  srglmhm  14158  srgrmhm  14159  ringpropd  14203  crngpropd  14204  ringlghm  14226  ringrghm  14227  mulgass3  14251  issubrng2  14378  subrngpropd  14384  issubrg2  14409  subrgintm  14411  subrgpropd  14421  rhmpropd  14422  unitrrg  14436  lmodprop2d  14545  islss3  14576  lssintclm  14581  qusrhm  14725  gsumfzfsum  14785  opnssneib  15070  neissex  15079  tgrest  15083  iscnp3  15117  cnpnei  15133  cnrest  15149  tx1cn  15183  txcnp  15185  elbl3ps  15308  elbl3  15309  blininf  15338  blssexps  15343  blssex  15344  blpnfctr  15353  mopni2  15397  blsscls2  15407  metss  15408  bdmet  15416  metrest  15420  metcn  15428  txmetcn  15433  bl2ioo  15464  ivthinclemlr  15551  ivthinclemur  15553  dvcj  15623  dvfre  15624  elplyd  15655  plyaddlem1  15661  plymullem1  15662  plymullem  15664  plycolemc  15672  plycjlemc  15674  coseq0q4123  15748  abssinper  15760  fsumdvdsmul  15908  lgsval2lem  15932  lgsval4lem  15933  lgsneg  15946  lgsmod  15948  lgsdir2  15955  lgsdir  15957  lgsne0  15960  lgssq  15962  lgsquadlem1  15999  usgredg2vlem2  16267  clwwlkccat  16445  clwwlknonex2lem2  16482  subctctexmid  16823  cvgcmp2n  16866  iswomninnlem  16883  nconstwlpo  16901