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  3879  intab  3977  pofun  4432  ralxfrd  4582  rexxfrd  4583  ordtri2or2exmidlem  4647  wessep  4699  poinxp  4818  relop  4904  fun11iun  5634  ssimaex  5737  fndmdif  5782  fconst2g  5898  foeqcnvco  5962  f1eqcocnv  5963  isocnv  5983  isocnv2  5984  riota2df  6024  caofdig  6299  f1o2ndf1  6423  tfr1onlembacc  6572  tfr1onlemaccex  6578  tfr1onlemres  6579  tfrcllembacc  6585  tfrcllemaccex  6591  tfrcllemres  6592  tfrcldm  6593  tfrcl  6594  xpdom2  7081  fimax2gtrilemstep  7157  xpfi  7191  eqsupti  7286  ordiso2  7325  enumctlemm  7404  enwomnilem  7459  cc2lem  7576  mulcanpig  7646  prarloclemlt  7804  genpdf  7819  genpdisj  7834  addnqprl  7840  addnqpru  7841  addlocpr  7847  prmuloc  7877  mulnqprl  7879  mulnqpru  7880  mullocpr  7882  ltpopr  7906  ltsopr  7907  ltaddpr  7908  ltexprlemdisj  7917  ltexprlemloc  7918  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  ltaprg  7930  recexprlemopu  7938  recexprlemloc  7942  cauappcvgprlemladdfl  7966  cauappcvgprlemladdru  7967  caucvgsrlemcau  8104  caucvgsrlemgt1  8106  caucvgsrlemoffcau  8109  caucvgsrlemoffres  8111  suplocsrlem  8119  axcaucvglemcau  8209  axpre-suploclemres  8212  axsuploc  8342  cnegexlem1  8444  cnegexlem3  8446  cnegex  8447  addsubeq4  8484  rimul  8855  divcanap6  8989  ltmul12a  9130  lemul12b  9131  lbinf  9218  zrevaddcl  9624  nzadd  9626  zextle  9665  fzind  9689  uz11  9873  infregelbex  9926  qreccl  9970  qrevaddcl  9972  irradd  9974  xrlttr  10124  xrltso  10125  xaddass  10198  xleadd1a  10202  xlt2add  10209  iccshftr  10323  iccshftl  10325  iccdil  10327  icccntr  10329  divelunit  10331  uzsubsubfz  10377  fzaddel  10389  fzrev  10414  elfzmlbp  10462  infssuzex  10589  zsupssdc  10594  frec2uzrdg  10767  frecuzrdgtcl  10770  frecuzrdgsuc  10772  frecuzrdgdomlem  10775  frecuzrdgfunlem  10777  frecuzrdgsuctlem  10781  iseqovex  10816  seq3val  10818  seqf  10822  seq3clss  10829  seq3fveq2  10833  seq3feq2  10834  seq3feq  10838  seq3shft2  10839  ser3mono  10845  seq3split  10846  seqsplitg  10847  seq3caopr3  10849  seq3caopr2  10851  seqcaopr2g  10852  iseqf1olemab  10860  seq3f1olemqsumkj  10869  seq3f1olemqsumk  10870  seq3f1olemqsum  10871  seq3f1olemstep  10872  seq3f1oleml  10874  seqf1oglem2a  10876  seqf1oglem2  10878  seq3id3  10882  seq3id  10883  seq3id2  10884  seq3homo  10885  seq3z  10886  seqfeq3  10887  seqhomog  10888  seqfeq4g  10889  ser3ge0  10894  expp1  10904  expnegap0  10905  expcllem  10908  mulexp  10936  expadd  10939  expaddzap  10941  expmulzap  10943  expdivap  10948  leexp1a  10952  expnlbnd  11022  bcpasc  11124  bccl  11125  hashfacen  11201  seq3coll  11207  ccatlen  11276  ccatvalfn  11282  ccatsymb  11283  ccatalpha  11294  pfxclz  11364  wrd2ind  11408  swrdccat  11420  seq3shft  11516  resqrexlemfp1  11687  sqrtdiv  11720  climshftlemg  11980  climcn1  11986  climsqz  12013  climsqz2  12014  clim2ser  12015  clim2ser2  12016  isermulc2  12018  climub  12022  serf0  12030  fsum3cvg  12057  sumrbdc  12058  summodclem3  12059  summodclem2a  12060  zsumdc  12063  fsumf1o  12069  isumss  12070  fisumss  12071  isumss2  12072  fsum3cvg2  12073  fsum3cvg3  12075  fsumcl2lem  12077  fsumcllem  12078  fsumadd  12085  fsumsplit  12086  fsumsplitsn  12089  sumsplitdc  12111  fisumrev2  12125  fsum2mul  12132  fsum00  12141  telfsumo  12145  fsumparts  12149  iserabs  12154  cvgratnnlemabsle  12206  cvgratnn  12210  cvgratz  12211  mertenslemub  12213  mertenslemi1  12214  mertenslem2  12215  mertensabs  12216  clim2prod  12218  clim2divap  12219  prodfap0  12224  prodfrecap  12225  prodeq2  12236  fproddccvg  12251  prodrbdclem2  12252  prodmodc  12257  zproddc  12258  fprodf1o  12267  fprodssdc  12269  fprodunsn  12283  fprodcllem  12285  fprodabs  12295  fprodeq0  12296  fprodmodd  12320  eftlcvg  12366  negdvdsb  12486  dvdsnegb  12487  fsumdvds  12521  dvdsext  12534  addmodlteqALT  12538  nno  12585  gcdsupex  12646  gcdsupcl  12647  bezoutlembz  12693  dvdssq  12720  eucalgf  12745  dvdslcm  12759  lcmledvds  12760  lcmeq0  12761  lcmcl  12762  lcmdvds  12769  lcmgcdeq  12773  divgcdcoprmex  12792  isprm5lem  12831  phibndlem  12906  phiprmpw  12912  pc2dvds  13021  pcmpt  13034  prmpwdvds  13046  1arith  13058  4sqleminfi  13088  ctiunctlemf  13178  ctiunct  13180  grpinva  13588  grprida  13589  gsumpropd2  13595  sgrppropd  13615  prdssgrpd  13617  mndpropd  13642  prdsidlem  13649  prdsmndd  13650  mhmpropd  13668  0mhm  13688  resmhm2  13690  resmhm2b  13691  grplcan  13764  mulgval  13828  mulgnn0z  13855  mulgnndir  13857  mulgnn0dir  13858  issubg2m  13895  issubg4m  13899  subgintm  13904  ghmf1  13979  gsumfzmptfidmadd  14045  gsumfzmhm  14049  srglmhm  14126  srgrmhm  14127  ringpropd  14171  crngpropd  14172  ringlghm  14194  ringrghm  14195  mulgass3  14218  issubrng2  14344  subrngpropd  14350  issubrg2  14375  subrgintm  14377  subrgpropd  14387  rhmpropd  14388  unitrrg  14402  lmodprop2d  14483  islss3  14514  lssintclm  14519  qusrhm  14663  gsumfzfsum  14723  opnssneib  15008  neissex  15017  tgrest  15021  iscnp3  15055  cnpnei  15071  cnrest  15087  tx1cn  15121  txcnp  15123  elbl3ps  15246  elbl3  15247  blininf  15276  blssexps  15281  blssex  15282  blpnfctr  15291  mopni2  15335  blsscls2  15345  metss  15346  bdmet  15354  metrest  15358  metcn  15366  txmetcn  15371  bl2ioo  15402  ivthinclemlr  15489  ivthinclemur  15491  dvcj  15561  dvfre  15562  elplyd  15593  plyaddlem1  15599  plymullem1  15600  plymullem  15602  plycolemc  15610  plycjlemc  15612  coseq0q4123  15686  abssinper  15698  fsumdvdsmul  15846  lgsval2lem  15870  lgsval4lem  15871  lgsneg  15884  lgsmod  15886  lgsdir2  15893  lgsdir  15895  lgsne0  15898  lgssq  15900  lgsquadlem1  15937  usgredg2vlem2  16205  clwwlkccat  16383  clwwlknonex2lem2  16420  subctctexmid  16761  cvgcmp2n  16804  iswomninnlem  16821  nconstwlpo  16838