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  1183  3ad2antl2  1184  ad4ant124  1240  3adant1r  1255  ad5ant235  1262  ad5ant135  1267  bilukdc  1438  elpr2elpr  3854  intab  3952  pofun  4404  ralxfrd  4554  rexxfrd  4555  ordtri2or2exmidlem  4619  wessep  4671  poinxp  4790  relop  4875  fun11iun  5598  ssimaex  5700  fndmdif  5745  fconst2g  5861  foeqcnvco  5923  f1eqcocnv  5924  isocnv  5944  isocnv2  5945  riota2df  5985  caofdig  6261  f1o2ndf1  6385  tfr1onlembacc  6499  tfr1onlemaccex  6505  tfr1onlemres  6506  tfrcllembacc  6512  tfrcllemaccex  6518  tfrcllemres  6519  tfrcldm  6520  tfrcl  6521  xpdom2  7003  fimax2gtrilemstep  7076  xpfi  7110  eqsupti  7179  ordiso2  7218  enumctlemm  7297  enwomnilem  7352  cc2lem  7468  mulcanpig  7538  prarloclemlt  7696  genpdf  7711  genpdisj  7726  addnqprl  7732  addnqpru  7733  addlocpr  7739  prmuloc  7769  mulnqprl  7771  mulnqpru  7772  mullocpr  7774  ltpopr  7798  ltsopr  7799  ltaddpr  7800  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  ltaprg  7822  recexprlemopu  7830  recexprlemloc  7834  cauappcvgprlemladdfl  7858  cauappcvgprlemladdru  7859  caucvgsrlemcau  7996  caucvgsrlemgt1  7998  caucvgsrlemoffcau  8001  caucvgsrlemoffres  8003  suplocsrlem  8011  axcaucvglemcau  8101  axpre-suploclemres  8104  axsuploc  8235  cnegexlem1  8337  cnegexlem3  8339  cnegex  8340  addsubeq4  8377  rimul  8748  divcanap6  8882  ltmul12a  9023  lemul12b  9024  lbinf  9111  zrevaddcl  9513  nzadd  9515  zextle  9554  fzind  9578  uz11  9762  infregelbex  9810  qreccl  9854  qrevaddcl  9856  irradd  9858  xrlttr  10008  xrltso  10009  xaddass  10082  xleadd1a  10086  xlt2add  10093  iccshftr  10207  iccshftl  10209  iccdil  10211  icccntr  10213  divelunit  10215  uzsubsubfz  10260  fzaddel  10272  fzrev  10297  elfzmlbp  10345  infssuzex  10470  zsupssdc  10475  frec2uzrdg  10648  frecuzrdgtcl  10651  frecuzrdgsuc  10653  frecuzrdgdomlem  10656  frecuzrdgfunlem  10658  frecuzrdgsuctlem  10662  iseqovex  10697  seq3val  10699  seqf  10703  seq3clss  10710  seq3fveq2  10714  seq3feq2  10715  seq3feq  10719  seq3shft2  10720  ser3mono  10726  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seq3caopr2  10732  seqcaopr2g  10733  iseqf1olemab  10741  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  seq3f1olemstep  10753  seq3f1oleml  10755  seqf1oglem2a  10757  seqf1oglem2  10759  seq3id3  10763  seq3id  10764  seq3id2  10765  seq3homo  10766  seq3z  10767  seqfeq3  10768  seqhomog  10769  seqfeq4g  10770  ser3ge0  10775  expp1  10785  expnegap0  10786  expcllem  10789  mulexp  10817  expadd  10820  expaddzap  10822  expmulzap  10824  expdivap  10829  leexp1a  10833  expnlbnd  10903  bcpasc  11005  bccl  11006  hashfacen  11076  seq3coll  11082  ccatlen  11148  ccatvalfn  11154  ccatsymb  11155  ccatalpha  11166  pfxclz  11232  wrd2ind  11276  swrdccat  11288  seq3shft  11370  resqrexlemfp1  11541  sqrtdiv  11574  climshftlemg  11834  climcn1  11840  climsqz  11867  climsqz2  11868  clim2ser  11869  clim2ser2  11870  isermulc2  11872  climub  11876  serf0  11884  fsum3cvg  11910  sumrbdc  11911  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsumf1o  11922  isumss  11923  fisumss  11924  isumss2  11925  fsum3cvg2  11926  fsum3cvg3  11928  fsumcl2lem  11930  fsumcllem  11931  fsumadd  11938  fsumsplit  11939  fsumsplitsn  11942  sumsplitdc  11964  fisumrev2  11978  fsum2mul  11985  fsum00  11994  telfsumo  11998  fsumparts  12002  iserabs  12007  cvgratnnlemabsle  12059  cvgratnn  12063  cvgratz  12064  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  clim2prod  12071  clim2divap  12072  prodfap0  12077  prodfrecap  12078  prodeq2  12089  fproddccvg  12104  prodrbdclem2  12105  prodmodc  12110  zproddc  12111  fprodf1o  12120  fprodssdc  12122  fprodunsn  12136  fprodcllem  12138  fprodabs  12148  fprodeq0  12149  fprodmodd  12173  eftlcvg  12219  negdvdsb  12339  dvdsnegb  12340  fsumdvds  12374  dvdsext  12387  addmodlteqALT  12391  nno  12438  gcdsupex  12499  gcdsupcl  12500  bezoutlembz  12546  dvdssq  12573  eucalgf  12598  dvdslcm  12612  lcmledvds  12613  lcmeq0  12614  lcmcl  12615  lcmdvds  12622  lcmgcdeq  12626  divgcdcoprmex  12645  isprm5lem  12684  phibndlem  12759  phiprmpw  12765  pc2dvds  12874  pcmpt  12887  prmpwdvds  12899  1arith  12911  4sqleminfi  12941  ctiunctlemf  13030  ctiunct  13032  grpinva  13440  grprida  13441  gsumpropd2  13447  sgrppropd  13467  prdssgrpd  13469  mndpropd  13494  prdsidlem  13501  prdsmndd  13502  mhmpropd  13520  0mhm  13540  resmhm2  13542  resmhm2b  13543  grplcan  13616  mulgval  13680  mulgnn0z  13707  mulgnndir  13709  mulgnn0dir  13710  issubg2m  13747  issubg4m  13751  subgintm  13756  ghmf1  13831  gsumfzmptfidmadd  13897  gsumfzmhm  13901  srglmhm  13977  srgrmhm  13978  ringpropd  14022  crngpropd  14023  ringlghm  14045  ringrghm  14046  mulgass3  14069  issubrng2  14195  subrngpropd  14201  issubrg2  14226  subrgintm  14228  subrgpropd  14238  rhmpropd  14239  unitrrg  14252  lmodprop2d  14333  islss3  14364  lssintclm  14369  qusrhm  14513  gsumfzfsum  14573  opnssneib  14851  neissex  14860  tgrest  14864  iscnp3  14898  cnpnei  14914  cnrest  14930  tx1cn  14964  txcnp  14966  elbl3ps  15089  elbl3  15090  blininf  15119  blssexps  15124  blssex  15125  blpnfctr  15134  mopni2  15178  blsscls2  15188  metss  15189  bdmet  15197  metrest  15201  metcn  15209  txmetcn  15214  bl2ioo  15245  ivthinclemlr  15332  ivthinclemur  15334  dvcj  15404  dvfre  15405  elplyd  15436  plyaddlem1  15442  plymullem1  15443  plymullem  15445  plycolemc  15453  plycjlemc  15455  coseq0q4123  15529  abssinper  15541  fsumdvdsmul  15686  lgsval2lem  15710  lgsval4lem  15711  lgsneg  15724  lgsmod  15726  lgsdir2  15733  lgsdir  15735  lgsne0  15738  lgssq  15740  lgsquadlem1  15777  usgredg2vlem2  16042  clwwlkccat  16170  subctctexmid  16479  cvgcmp2n  16515  iswomninnlem  16531  nconstwlpo  16548