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  1162  3ad2antl2  1163  ad4ant124  1219  3adant1r  1234  ad5ant235  1241  ad5ant135  1246  bilukdc  1416  intab  3916  pofun  4363  ralxfrd  4513  rexxfrd  4514  ordtri2or2exmidlem  4578  wessep  4630  poinxp  4748  relop  4832  fun11iun  5550  ssimaex  5647  fndmdif  5692  fconst2g  5806  foeqcnvco  5866  f1eqcocnv  5867  isocnv  5887  isocnv2  5888  riota2df  5927  caofdig  6199  f1o2ndf1  6321  tfr1onlembacc  6435  tfr1onlemaccex  6441  tfr1onlemres  6442  tfrcllembacc  6448  tfrcllemaccex  6454  tfrcllemres  6455  tfrcldm  6456  tfrcl  6457  xpdom2  6933  fimax2gtrilemstep  7004  xpfi  7036  eqsupti  7105  ordiso2  7144  enumctlemm  7223  enwomnilem  7278  cc2lem  7385  mulcanpig  7455  prarloclemlt  7613  genpdf  7628  genpdisj  7643  addnqprl  7649  addnqpru  7650  addlocpr  7656  prmuloc  7686  mulnqprl  7688  mulnqpru  7689  mullocpr  7691  ltpopr  7715  ltsopr  7716  ltaddpr  7717  ltexprlemdisj  7726  ltexprlemloc  7727  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  ltaprg  7739  recexprlemopu  7747  recexprlemloc  7751  cauappcvgprlemladdfl  7775  cauappcvgprlemladdru  7776  caucvgsrlemcau  7913  caucvgsrlemgt1  7915  caucvgsrlemoffcau  7918  caucvgsrlemoffres  7920  suplocsrlem  7928  axcaucvglemcau  8018  axpre-suploclemres  8021  axsuploc  8152  cnegexlem1  8254  cnegexlem3  8256  cnegex  8257  addsubeq4  8294  rimul  8665  divcanap6  8799  ltmul12a  8940  lemul12b  8941  lbinf  9028  zrevaddcl  9430  nzadd  9432  zextle  9471  fzind  9495  uz11  9678  infregelbex  9726  qreccl  9770  qrevaddcl  9772  irradd  9774  xrlttr  9924  xrltso  9925  xaddass  9998  xleadd1a  10002  xlt2add  10009  iccshftr  10123  iccshftl  10125  iccdil  10127  icccntr  10129  divelunit  10131  uzsubsubfz  10176  fzaddel  10188  fzrev  10213  elfzmlbp  10261  infssuzex  10383  zsupssdc  10388  frec2uzrdg  10561  frecuzrdgtcl  10564  frecuzrdgsuc  10566  frecuzrdgdomlem  10569  frecuzrdgfunlem  10571  frecuzrdgsuctlem  10575  iseqovex  10610  seq3val  10612  seqf  10616  seq3clss  10623  seq3fveq2  10627  seq3feq2  10628  seq3feq  10632  seq3shft2  10633  ser3mono  10639  seq3split  10640  seqsplitg  10641  seq3caopr3  10643  seq3caopr2  10645  seqcaopr2g  10646  iseqf1olemab  10654  seq3f1olemqsumkj  10663  seq3f1olemqsumk  10664  seq3f1olemqsum  10665  seq3f1olemstep  10666  seq3f1oleml  10668  seqf1oglem2a  10670  seqf1oglem2  10672  seq3id3  10676  seq3id  10677  seq3id2  10678  seq3homo  10679  seq3z  10680  seqfeq3  10681  seqhomog  10682  seqfeq4g  10683  ser3ge0  10688  expp1  10698  expnegap0  10699  expcllem  10702  mulexp  10730  expadd  10733  expaddzap  10735  expmulzap  10737  expdivap  10742  leexp1a  10746  expnlbnd  10816  bcpasc  10918  bccl  10919  hashfacen  10988  seq3coll  10994  ccatlen  11059  ccatvalfn  11065  ccatsymb  11066  seq3shft  11193  resqrexlemfp1  11364  sqrtdiv  11397  climshftlemg  11657  climcn1  11663  climsqz  11690  climsqz2  11691  clim2ser  11692  clim2ser2  11693  isermulc2  11695  climub  11699  serf0  11707  fsum3cvg  11733  sumrbdc  11734  summodclem3  11735  summodclem2a  11736  zsumdc  11739  fsumf1o  11745  isumss  11746  fisumss  11747  isumss2  11748  fsum3cvg2  11749  fsum3cvg3  11751  fsumcl2lem  11753  fsumcllem  11754  fsumadd  11761  fsumsplit  11762  fsumsplitsn  11765  sumsplitdc  11787  fisumrev2  11801  fsum2mul  11808  fsum00  11817  telfsumo  11821  fsumparts  11825  iserabs  11830  cvgratnnlemabsle  11882  cvgratnn  11886  cvgratz  11887  mertenslemub  11889  mertenslemi1  11890  mertenslem2  11891  mertensabs  11892  clim2prod  11894  clim2divap  11895  prodfap0  11900  prodfrecap  11901  prodeq2  11912  fproddccvg  11927  prodrbdclem2  11928  prodmodc  11933  zproddc  11934  fprodf1o  11943  fprodssdc  11945  fprodunsn  11959  fprodcllem  11961  fprodabs  11971  fprodeq0  11972  fprodmodd  11996  eftlcvg  12042  negdvdsb  12162  dvdsnegb  12163  fsumdvds  12197  dvdsext  12210  addmodlteqALT  12214  nno  12261  gcdsupex  12322  gcdsupcl  12323  bezoutlembz  12369  dvdssq  12396  eucalgf  12421  dvdslcm  12435  lcmledvds  12436  lcmeq0  12437  lcmcl  12438  lcmdvds  12445  lcmgcdeq  12449  divgcdcoprmex  12468  isprm5lem  12507  phibndlem  12582  phiprmpw  12588  pc2dvds  12697  pcmpt  12710  prmpwdvds  12722  1arith  12734  4sqleminfi  12764  ctiunctlemf  12853  ctiunct  12855  grpinva  13262  grprida  13263  gsumpropd2  13269  sgrppropd  13289  prdssgrpd  13291  mndpropd  13316  prdsidlem  13323  prdsmndd  13324  mhmpropd  13342  0mhm  13362  resmhm2  13364  resmhm2b  13365  grplcan  13438  mulgval  13502  mulgnn0z  13529  mulgnndir  13531  mulgnn0dir  13532  issubg2m  13569  issubg4m  13573  subgintm  13578  ghmf1  13653  gsumfzmptfidmadd  13719  gsumfzmhm  13723  srglmhm  13799  srgrmhm  13800  ringpropd  13844  crngpropd  13845  ringlghm  13867  ringrghm  13868  mulgass3  13891  issubrng2  14016  subrngpropd  14022  issubrg2  14047  subrgintm  14049  subrgpropd  14059  rhmpropd  14060  unitrrg  14073  lmodprop2d  14154  islss3  14185  lssintclm  14190  qusrhm  14334  gsumfzfsum  14394  opnssneib  14672  neissex  14681  tgrest  14685  iscnp3  14719  cnpnei  14735  cnrest  14751  tx1cn  14785  txcnp  14787  elbl3ps  14910  elbl3  14911  blininf  14940  blssexps  14945  blssex  14946  blpnfctr  14955  mopni2  14999  blsscls2  15009  metss  15010  bdmet  15018  metrest  15022  metcn  15030  txmetcn  15035  bl2ioo  15066  ivthinclemlr  15153  ivthinclemur  15155  dvcj  15225  dvfre  15226  elplyd  15257  plyaddlem1  15263  plymullem1  15264  plymullem  15266  plycolemc  15274  plycjlemc  15276  coseq0q4123  15350  abssinper  15362  fsumdvdsmul  15507  lgsval2lem  15531  lgsval4lem  15532  lgsneg  15545  lgsmod  15547  lgsdir2  15554  lgsdir  15556  lgsne0  15559  lgssq  15561  lgsquadlem1  15598  subctctexmid  16011  cvgcmp2n  16046  iswomninnlem  16062  nconstwlpo  16079