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 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used 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  3901  intab  3999  pofun  4457  ralxfrd  4608  rexxfrd  4609  ordtri2or2exmidlem  4673  wessep  4725  poinxp  4844  relop  4930  fun11iun  5660  relndmfv  5728  ssimaex  5764  fndmdif  5814  fconst2g  5930  foeqcnvco  5996  f1eqcocnv  5997  isocnv  6017  isocnv2  6018  riota2df  6060  caofdig  6336  f1o2ndf1  6464  tfr1onlembacc  6613  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllembacc  6626  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfrcl  6635  xpdom2  7129  fimax2gtrilemstep  7205  xpfi  7239  eqsupti  7336  ordiso2  7375  enumctlemm  7454  enwomnilem  7509  cc2lem  7632  mulcanpig  7702  prarloclemlt  7860  genpdf  7875  genpdisj  7890  addnqprl  7896  addnqpru  7897  addlocpr  7903  prmuloc  7933  mulnqprl  7935  mulnqpru  7936  mullocpr  7938  ltpopr  7962  ltsopr  7963  ltaddpr  7964  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprg  7986  recexprlemopu  7994  recexprlemloc  7998  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  suplocsrlem  8175  axcaucvglemcau  8265  axpre-suploclemres  8268  axsuploc  8398  cnegexlem1  8501  cnegexlem3  8503  cnegex  8504  addsubeq4  8541  rimul  8914  divcanap6  9050  ltmul12a  9191  lemul12b  9192  lbinf  9279  zrevaddcl  9697  nzadd  9699  zextle  9739  fzind  9763  uz11  9947  infregelbex  10000  qreccl  10044  qrevaddcl  10046  irradd  10048  xrlttr  10199  xrltso  10200  xaddass  10273  xleadd1a  10277  xlt2add  10284  iccshftr  10398  iccshftl  10400  iccdil  10402  icccntr  10404  divelunit  10406  uzsubsubfz  10454  fzaddel  10467  fzrev  10493  elfzmlbp  10541  infssuzex  10668  zsupssdc  10675  frec2uzrdg  10848  frecuzrdgtcl  10851  frecuzrdgsuc  10853  frecuzrdgdomlem  10856  frecuzrdgfunlem  10858  frecuzrdgsuctlem  10862  iseqovex  10897  seq3val  10899  seqf  10903  seq3clss  10910  seq3fveq2  10914  seq3feq2  10915  seq3feq  10919  seq3shft2  10920  ser3mono  10926  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  seq3caopr2  10932  seqcaopr2g  10933  iseqf1olemab  10941  seq3f1olemqsumkj  10950  seq3f1olemqsumk  10951  seq3f1olemqsum  10952  seq3f1olemstep  10953  seq3f1oleml  10955  seqf1oglem2a  10957  seqf1oglem2  10959  seq3id3  10963  seq3id  10964  seq3id2  10965  seq3homo  10966  seq3z  10967  seqfeq3  10968  seqhomog  10969  seqfeq4g  10970  ser3ge0  10975  expp1  10985  expnegap0  10986  expcllem  10989  mulexp  11017  expadd  11020  expaddzap  11022  expmulzap  11024  expdivap  11029  leexp1a  11033  expnlbnd  11104  bcpasc  11206  bccl  11207  hashfacen  11286  seq3coll  11296  ccatlen  11365  ccatvalfn  11371  ccatsymb  11372  ccatalpha  11383  pfxclz  11453  wrd2ind  11497  swrdccat  11509  seq3shft  11605  resqrexlemfp1  11777  sqrtdiv  11810  climshftlemg  12070  climcn1  12076  climsqz  12103  climsqz2  12104  clim2ser  12105  clim2ser2  12106  isermulc2  12108  climub  12112  serf0  12120  fsum3cvg  12147  sumrbdc  12148  summodclem3  12149  summodclem2a  12150  zsumdc  12153  fsumf1o  12159  isumss  12160  fisumss  12161  isumss2  12162  fsum3cvg2  12163  fsum3cvg3  12165  fsumcl2lem  12167  fsumcllem  12168  fsumadd  12175  fsumsplit  12176  fsumsplitsn  12179  sumsplitdc  12201  fisumrev2  12215  fsum2mul  12222  fsum00  12231  telfsumo  12235  fsumparts  12239  iserabs  12244  cvgratnnlemabsle  12296  cvgratnn  12300  cvgratz  12301  mertenslemub  12303  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  clim2prod  12308  clim2divap  12309  prodfap0  12314  prodfrecap  12315  prodeq2  12326  fproddccvg  12341  prodrbdclem2  12342  prodmodc  12347  zproddc  12348  fprodf1o  12357  fprodssdc  12359  fprodunsn  12373  fprodcllem  12375  fprodabs  12385  fprodeq0  12386  fprodmodd  12410  eftlcvg  12456  negdvdsb  12576  dvdsnegb  12577  fsumdvds  12611  dvdsext  12624  addmodlteqALT  12628  nno  12675  gcdsupex  12736  gcdsupcl  12737  bezoutlembz  12783  dvdssq  12810  eucalgf  12835  dvdslcm  12849  lcmledvds  12850  lcmeq0  12851  lcmcl  12852  lcmdvds  12859  lcmgcdeq  12863  divgcdcoprmex  12882  isprm5lem  12921  phibndlem  12996  phiprmpw  13002  pc2dvds  13111  pcmpt  13124  prmpwdvds  13136  1arith  13148  4sqleminfi  13178  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemsv  13255  ballotfilemsima  13261  ctiunctlemf  13331  ctiunct  13333  grpinva  13708  grprida  13709  sgrppropd  13730  mndpropd  13755  mhmpropd  13775  0mhm  13795  resmhm2  13797  resmhm2b  13798  grplcan  13869  mulgval  13927  mulgnn0z  13954  mulgnndir  13956  mulgnn0dir  13957  issubg2m  13994  issubg4m  13998  subgintm  14003  ghmf1  14078  gzsummhm  14147  gsumressfi  14169  prdssgrpd  14193  prdsidlem  14195  prdsmndd  14196  srglmhm  14299  srgrmhm  14300  ringpropd  14345  crngpropd  14346  ringlghm  14368  ringrghm  14369  mulgass3  14393  issubrng2  14520  subrngpropd  14526  issubrg2  14551  subrgintm  14553  subrgpropd  14563  rhmpropd  14564  unitrrg  14578  lmodprop2d  14687  islss3  14718  lssintclm  14723  qusrhm  14867  issubassa3  15014  opnssneib  15259  neissex  15268  tgrest  15272  iscnp3  15306  cnpnei  15322  cnrest  15338  tx1cn  15372  txcnp  15374  elbl3ps  15497  elbl3  15498  blininf  15527  blssexps  15532  blssex  15533  blpnfctr  15542  mopni2  15586  blsscls2  15596  metss  15597  bdmet  15605  metrest  15609  metcn  15617  txmetcn  15622  bl2ioo  15653  ivthinclemlr  15740  ivthinclemur  15742  dvcj  15812  dvfre  15813  elplyd  15844  plyaddlem1  15850  plymullem1  15851  plymullem  15853  plycolemc  15861  plycjlemc  15863  coseq0q4123  15938  abssinper  15950  fsumdvdsmul  16111  lgsval2lem  16141  lgsval4lem  16142  lgsneg  16155  lgsmod  16157  lgsdir2  16164  lgsdir  16166  lgsne0  16169  lgssq  16171  lgsquadlem1  16208  usgredg2vlem2  16476  clwwlkccat  16654  clwwlknonex2lem2  16691  subctctexmid  17042  cvgcmp2n  17094  iswomninnlem  17111  nconstwlpo  17128