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  3860  intab  3958  pofun  4411  ralxfrd  4561  rexxfrd  4562  ordtri2or2exmidlem  4626  wessep  4678  poinxp  4797  relop  4882  fun11iun  5607  ssimaex  5710  fndmdif  5755  fconst2g  5872  foeqcnvco  5936  f1eqcocnv  5937  isocnv  5957  isocnv2  5958  riota2df  5998  caofdig  6274  f1o2ndf1  6398  tfr1onlembacc  6513  tfr1onlemaccex  6519  tfr1onlemres  6520  tfrcllembacc  6526  tfrcllemaccex  6532  tfrcllemres  6533  tfrcldm  6534  tfrcl  6535  xpdom2  7020  fimax2gtrilemstep  7095  xpfi  7129  eqsupti  7200  ordiso2  7239  enumctlemm  7318  enwomnilem  7373  cc2lem  7490  mulcanpig  7560  prarloclemlt  7718  genpdf  7733  genpdisj  7748  addnqprl  7754  addnqpru  7755  addlocpr  7761  prmuloc  7791  mulnqprl  7793  mulnqpru  7794  mullocpr  7796  ltpopr  7820  ltsopr  7821  ltaddpr  7822  ltexprlemdisj  7831  ltexprlemloc  7832  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  ltaprg  7844  recexprlemopu  7852  recexprlemloc  7856  cauappcvgprlemladdfl  7880  cauappcvgprlemladdru  7881  caucvgsrlemcau  8018  caucvgsrlemgt1  8020  caucvgsrlemoffcau  8023  caucvgsrlemoffres  8025  suplocsrlem  8033  axcaucvglemcau  8123  axpre-suploclemres  8126  axsuploc  8257  cnegexlem1  8359  cnegexlem3  8361  cnegex  8362  addsubeq4  8399  rimul  8770  divcanap6  8904  ltmul12a  9045  lemul12b  9046  lbinf  9133  zrevaddcl  9535  nzadd  9537  zextle  9576  fzind  9600  uz11  9784  infregelbex  9837  qreccl  9881  qrevaddcl  9883  irradd  9885  xrlttr  10035  xrltso  10036  xaddass  10109  xleadd1a  10113  xlt2add  10120  iccshftr  10234  iccshftl  10236  iccdil  10238  icccntr  10240  divelunit  10242  uzsubsubfz  10287  fzaddel  10299  fzrev  10324  elfzmlbp  10372  infssuzex  10499  zsupssdc  10504  frec2uzrdg  10677  frecuzrdgtcl  10680  frecuzrdgsuc  10682  frecuzrdgdomlem  10685  frecuzrdgfunlem  10687  frecuzrdgsuctlem  10691  iseqovex  10726  seq3val  10728  seqf  10732  seq3clss  10739  seq3fveq2  10743  seq3feq2  10744  seq3feq  10748  seq3shft2  10749  ser3mono  10755  seq3split  10756  seqsplitg  10757  seq3caopr3  10759  seq3caopr2  10761  seqcaopr2g  10762  iseqf1olemab  10770  seq3f1olemqsumkj  10779  seq3f1olemqsumk  10780  seq3f1olemqsum  10781  seq3f1olemstep  10782  seq3f1oleml  10784  seqf1oglem2a  10786  seqf1oglem2  10788  seq3id3  10792  seq3id  10793  seq3id2  10794  seq3homo  10795  seq3z  10796  seqfeq3  10797  seqhomog  10798  seqfeq4g  10799  ser3ge0  10804  expp1  10814  expnegap0  10815  expcllem  10818  mulexp  10846  expadd  10849  expaddzap  10851  expmulzap  10853  expdivap  10858  leexp1a  10862  expnlbnd  10932  bcpasc  11034  bccl  11035  hashfacen  11106  seq3coll  11112  ccatlen  11181  ccatvalfn  11187  ccatsymb  11188  ccatalpha  11199  pfxclz  11269  wrd2ind  11313  swrdccat  11325  seq3shft  11421  resqrexlemfp1  11592  sqrtdiv  11625  climshftlemg  11885  climcn1  11891  climsqz  11918  climsqz2  11919  clim2ser  11920  clim2ser2  11921  isermulc2  11923  climub  11927  serf0  11935  fsum3cvg  11962  sumrbdc  11963  summodclem3  11964  summodclem2a  11965  zsumdc  11968  fsumf1o  11974  isumss  11975  fisumss  11976  isumss2  11977  fsum3cvg2  11978  fsum3cvg3  11980  fsumcl2lem  11982  fsumcllem  11983  fsumadd  11990  fsumsplit  11991  fsumsplitsn  11994  sumsplitdc  12016  fisumrev2  12030  fsum2mul  12037  fsum00  12046  telfsumo  12050  fsumparts  12054  iserabs  12059  cvgratnnlemabsle  12111  cvgratnn  12115  cvgratz  12116  mertenslemub  12118  mertenslemi1  12119  mertenslem2  12120  mertensabs  12121  clim2prod  12123  clim2divap  12124  prodfap0  12129  prodfrecap  12130  prodeq2  12141  fproddccvg  12156  prodrbdclem2  12157  prodmodc  12162  zproddc  12163  fprodf1o  12172  fprodssdc  12174  fprodunsn  12188  fprodcllem  12190  fprodabs  12200  fprodeq0  12201  fprodmodd  12225  eftlcvg  12271  negdvdsb  12391  dvdsnegb  12392  fsumdvds  12426  dvdsext  12439  addmodlteqALT  12443  nno  12490  gcdsupex  12551  gcdsupcl  12552  bezoutlembz  12598  dvdssq  12625  eucalgf  12650  dvdslcm  12664  lcmledvds  12665  lcmeq0  12666  lcmcl  12667  lcmdvds  12674  lcmgcdeq  12678  divgcdcoprmex  12697  isprm5lem  12736  phibndlem  12811  phiprmpw  12817  pc2dvds  12926  pcmpt  12939  prmpwdvds  12951  1arith  12963  4sqleminfi  12993  ctiunctlemf  13082  ctiunct  13084  grpinva  13492  grprida  13493  gsumpropd2  13499  sgrppropd  13519  prdssgrpd  13521  mndpropd  13546  prdsidlem  13553  prdsmndd  13554  mhmpropd  13572  0mhm  13592  resmhm2  13594  resmhm2b  13595  grplcan  13668  mulgval  13732  mulgnn0z  13759  mulgnndir  13761  mulgnn0dir  13762  issubg2m  13799  issubg4m  13803  subgintm  13808  ghmf1  13883  gsumfzmptfidmadd  13949  gsumfzmhm  13953  srglmhm  14030  srgrmhm  14031  ringpropd  14075  crngpropd  14076  ringlghm  14098  ringrghm  14099  mulgass3  14122  issubrng2  14248  subrngpropd  14254  issubrg2  14279  subrgintm  14281  subrgpropd  14291  rhmpropd  14292  unitrrg  14305  lmodprop2d  14386  islss3  14417  lssintclm  14422  qusrhm  14566  gsumfzfsum  14626  opnssneib  14909  neissex  14918  tgrest  14922  iscnp3  14956  cnpnei  14972  cnrest  14988  tx1cn  15022  txcnp  15024  elbl3ps  15147  elbl3  15148  blininf  15177  blssexps  15182  blssex  15183  blpnfctr  15192  mopni2  15236  blsscls2  15246  metss  15247  bdmet  15255  metrest  15259  metcn  15267  txmetcn  15272  bl2ioo  15303  ivthinclemlr  15390  ivthinclemur  15392  dvcj  15462  dvfre  15463  elplyd  15494  plyaddlem1  15500  plymullem1  15501  plymullem  15503  plycolemc  15511  plycjlemc  15513  coseq0q4123  15587  abssinper  15599  fsumdvdsmul  15744  lgsval2lem  15768  lgsval4lem  15769  lgsneg  15782  lgsmod  15784  lgsdir2  15791  lgsdir  15793  lgsne0  15796  lgssq  15798  lgsquadlem1  15835  usgredg2vlem2  16103  clwwlkccat  16281  clwwlknonex2lem2  16318  subctctexmid  16661  cvgcmp2n  16704  iswomninnlem  16721  nconstwlpo  16738