Theorem adantlr 481

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  492  ad2ant2r  513  ad2ant2rl  515  adantl3r  516  ad4ant14  518  ad4ant24  520  ad5ant13  523  ad5ant14  524  ad5ant15  525  3ad2antl1  1190  3ad2antl2  1191  ad4ant124  1247  3adant1r  1262  ad5ant235  1269  ad5ant135  1274  bilukdc  1445  ifeqeqxdc  3687  elpr2elpr  3899  intab  3997  pofun  4455  ralxfrd  4606  rexxfrd  4607  ordtri2or2exmidlem  4671  wessep  4723  poinxp  4842  relop  4928  fun11iun  5658  ssimaex  5761  fndmdif  5808  fconst2g  5924  foeqcnvco  5990  f1eqcocnv  5991  isocnv  6011  isocnv2  6012  riota2df  6054  caofdig  6330  f1o2ndf1  6458  tfr1onlembacc  6607  tfr1onlemaccex  6613  tfr1onlemres  6614  tfrcllembacc  6620  tfrcllemaccex  6626  tfrcllemres  6627  tfrcldm  6628  tfrcl  6629  xpdom2  7123  fimax2gtrilemstep  7199  xpfi  7233  eqsupti  7330  ordiso2  7369  enumctlemm  7448  enwomnilem  7503  cc2lem  7626  mulcanpig  7696  prarloclemlt  7854  genpdf  7869  genpdisj  7884  addnqprl  7890  addnqpru  7891  addlocpr  7897  prmuloc  7927  mulnqprl  7929  mulnqpru  7930  mullocpr  7932  ltpopr  7956  ltsopr  7957  ltaddpr  7958  ltexprlemdisj  7967  ltexprlemloc  7968  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  ltaprg  7980  recexprlemopu  7988  recexprlemloc  7992  cauappcvgprlemladdfl  8016  cauappcvgprlemladdru  8017  caucvgsrlemcau  8154  caucvgsrlemgt1  8156  caucvgsrlemoffcau  8159  caucvgsrlemoffres  8161  suplocsrlem  8169  axcaucvglemcau  8259  axpre-suploclemres  8262  axsuploc  8392  cnegexlem1  8495  cnegexlem3  8497  cnegex  8498  addsubeq4  8535  rimul  8907  divcanap6  9043  ltmul12a  9184  lemul12b  9185  lbinf  9272  zrevaddcl  9678  nzadd  9680  zextle  9720  fzind  9744  uz11  9928  infregelbex  9981  qreccl  10025  qrevaddcl  10027  irradd  10029  xrlttr  10180  xrltso  10181  xaddass  10254  xleadd1a  10258  xlt2add  10265  iccshftr  10379  iccshftl  10381  iccdil  10383  icccntr  10385  divelunit  10387  uzsubsubfz  10435  fzaddel  10448  fzrev  10474  elfzmlbp  10522  infssuzex  10649  zsupssdc  10656  frec2uzrdg  10829  frecuzrdgtcl  10832  frecuzrdgsuc  10834  frecuzrdgdomlem  10837  frecuzrdgfunlem  10839  frecuzrdgsuctlem  10843  iseqovex  10878  seq3val  10880  seqf  10884  seq3clss  10891  seq3fveq2  10895  seq3feq2  10896  seq3feq  10900  seq3shft2  10901  ser3mono  10907  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  seq3caopr2  10913  seqcaopr2g  10914  iseqf1olemab  10922  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seq3f1olemqsum  10933  seq3f1olemstep  10934  seq3f1oleml  10936  seqf1oglem2a  10938  seqf1oglem2  10940  seq3id3  10944  seq3id  10945  seq3id2  10946  seq3homo  10947  seq3z  10948  seqfeq3  10949  seqhomog  10950  seqfeq4g  10951  ser3ge0  10956  expp1  10966  expnegap0  10967  expcllem  10970  mulexp  10998  expadd  11001  expaddzap  11003  expmulzap  11005  expdivap  11010  leexp1a  11014  expnlbnd  11085  bcpasc  11187  bccl  11188  hashfacen  11267  seq3coll  11277  ccatlen  11346  ccatvalfn  11352  ccatsymb  11353  ccatalpha  11364  pfxclz  11434  wrd2ind  11478  swrdccat  11490  seq3shft  11586  resqrexlemfp1  11758  sqrtdiv  11791  climshftlemg  12051  climcn1  12057  climsqz  12084  climsqz2  12085  clim2ser  12086  clim2ser2  12087  isermulc2  12089  climub  12093  serf0  12101  fsum3cvg  12128  sumrbdc  12129  summodclem3  12130  summodclem2a  12131  zsumdc  12134  fsumf1o  12140  isumss  12141  fisumss  12142  isumss2  12143  fsum3cvg2  12144  fsum3cvg3  12146  fsumcl2lem  12148  fsumcllem  12149  fsumadd  12156  fsumsplit  12157  fsumsplitsn  12160  sumsplitdc  12182  fisumrev2  12196  fsum2mul  12203  fsum00  12212  telfsumo  12216  fsumparts  12220  iserabs  12225  cvgratnnlemabsle  12277  cvgratnn  12281  cvgratz  12282  mertenslemub  12284  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  clim2prod  12289  clim2divap  12290  prodfap0  12295  prodfrecap  12296  prodeq2  12307  fproddccvg  12322  prodrbdclem2  12323  prodmodc  12328  zproddc  12329  fprodf1o  12338  fprodssdc  12340  fprodunsn  12354  fprodcllem  12356  fprodabs  12366  fprodeq0  12367  fprodmodd  12391  eftlcvg  12437  negdvdsb  12557  dvdsnegb  12558  fsumdvds  12592  dvdsext  12605  addmodlteqALT  12609  nno  12656  gcdsupex  12717  gcdsupcl  12718  bezoutlembz  12764  dvdssq  12791  eucalgf  12816  dvdslcm  12830  lcmledvds  12831  lcmeq0  12832  lcmcl  12833  lcmdvds  12840  lcmgcdeq  12844  divgcdcoprmex  12863  isprm5lem  12902  phibndlem  12977  phiprmpw  12983  pc2dvds  13092  pcmpt  13105  prmpwdvds  13117  1arith  13129  4sqleminfi  13159  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemsv  13236  ballotfilemsima  13242  ctiunctlemf  13312  ctiunct  13314  grpinva  13689  grprida  13690  sgrppropd  13711  mndpropd  13736  mhmpropd  13756  0mhm  13776  resmhm2  13778  resmhm2b  13779  grplcan  13850  mulgval  13908  mulgnn0z  13935  mulgnndir  13937  mulgnn0dir  13938  issubg2m  13975  issubg4m  13979  subgintm  13984  ghmf1  14059  gzsummhm  14128  gsumressfi  14150  prdssgrpd  14174  prdsidlem  14176  prdsmndd  14177  srglmhm  14280  srgrmhm  14281  ringpropd  14326  crngpropd  14327  ringlghm  14349  ringrghm  14350  mulgass3  14374  issubrng2  14501  subrngpropd  14507  issubrg2  14532  subrgintm  14534  subrgpropd  14544  rhmpropd  14545  unitrrg  14559  lmodprop2d  14668  islss3  14699  lssintclm  14704  qusrhm  14848  issubassa3  14995  opnssneib  15240  neissex  15249  tgrest  15253  iscnp3  15287  cnpnei  15303  cnrest  15319  tx1cn  15353  txcnp  15355  elbl3ps  15478  elbl3  15479  blininf  15508  blssexps  15513  blssex  15514  blpnfctr  15523  mopni2  15567  blsscls2  15577  metss  15578  bdmet  15586  metrest  15590  metcn  15598  txmetcn  15603  bl2ioo  15634  ivthinclemlr  15721  ivthinclemur  15723  dvcj  15793  dvfre  15794  elplyd  15825  plyaddlem1  15831  plymullem1  15832  plymullem  15834  plycolemc  15842  plycjlemc  15844  coseq0q4123  15918  abssinper  15930  fsumdvdsmul  16088  lgsval2lem  16112  lgsval4lem  16113  lgsneg  16126  lgsmod  16128  lgsdir2  16135  lgsdir  16137  lgsne0  16140  lgssq  16142  lgsquadlem1  16179  usgredg2vlem2  16447  clwwlkccat  16625  clwwlknonex2lem2  16662  subctctexmid  17013  cvgcmp2n  17056  iswomninnlem  17073  nconstwlpo  17090