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  7337  ordiso2  7376  enumctlemm  7455  enwomnilem  7510  cc2lem  7633  mulcanpig  7703  prarloclemlt  7861  genpdf  7876  genpdisj  7891  addnqprl  7897  addnqpru  7898  addlocpr  7904  prmuloc  7934  mulnqprl  7936  mulnqpru  7937  mullocpr  7939  ltpopr  7963  ltsopr  7964  ltaddpr  7965  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltaprg  7987  recexprlemopu  7995  recexprlemloc  7999  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  suplocsrlem  8176  axcaucvglemcau  8266  axpre-suploclemres  8269  axsuploc  8399  cnegexlem1  8503  cnegexlem3  8505  cnegex  8506  addsubeq4  8543  rimul  8916  divcanap6  9052  ltmul12a  9193  lemul12b  9194  lbinf  9281  zrevaddcl  9700  nzadd  9702  zextle  9742  fzind  9766  uz11  9955  infregelbex  10008  qreccl  10052  qrevaddcl  10054  irradd  10056  xrlttr  10208  xrltso  10209  xaddass  10282  xleadd1a  10286  xlt2add  10293  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  divelunit  10415  uzsubsubfz  10463  fzaddel  10476  fzrev  10502  elfzmlbp  10550  infssuzex  10677  zsupssdc  10684  frec2uzrdg  10861  frecuzrdgtcl  10864  frecuzrdgsuc  10866  frecuzrdgdomlem  10869  frecuzrdgfunlem  10871  frecuzrdgsuctlem  10875  iseqovex  10910  seq3val  10912  seqf  10916  seq3clss  10923  seq3fveq2  10927  seq3feq2  10928  seq3feq  10932  seq3shft2  10933  ser3mono  10939  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemab  10954  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1oleml  10968  seqf1oglem2a  10970  seqf1oglem2  10972  seq3id3  10976  seq3id  10977  seq3id2  10978  seq3homo  10979  seq3z  10980  seqfeq3  10981  seqhomog  10982  seqfeq4g  10983  ser3ge0  10988  expp1  10998  expnegap0  10999  expcllem  11002  mulexp  11030  expadd  11033  expaddzap  11035  expmulzap  11037  expdivap  11042  leexp1a  11046  expnlbnd  11117  bcpasc  11220  bccl  11221  hashfacen  11300  seq3coll  11310  ccatlen  11379  ccatvalfn  11385  ccatsymb  11386  ccatalpha  11397  pfxclz  11467  wrd2ind  11511  swrdccat  11523  seq3shft  11619  resqrexlemfp1  11791  sqrtdiv  11824  climshftlemg  12087  climcn1  12093  climsqz  12120  climsqz2  12121  clim2ser  12122  clim2ser2  12123  isermulc2  12125  climub  12129  serf0  12137  fsum3cvg  12164  sumrbdc  12165  summodclem3  12166  summodclem2a  12167  zsumdc  12170  fsumf1o  12176  isumss  12177  fisumss  12178  isumss2  12179  fsum3cvg2  12180  fsum3cvg3  12182  fsumcl2lem  12184  fsumcllem  12185  fsumadd  12192  fsumsplit  12193  fsumsplitsn  12196  sumsplitdc  12218  fisumrev2  12232  fsum2mul  12239  fsum00  12248  telfsumo  12252  fsumparts  12256  iserabs  12261  cvgratnnlemabsle  12313  cvgratnn  12317  cvgratz  12318  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  clim2prod  12325  clim2divap  12326  prodfap0  12331  prodfrecap  12332  prodeq2  12343  fproddccvg  12358  prodrbdclem2  12359  prodmodc  12364  zproddc  12365  fprodf1o  12374  fprodssdc  12376  fprodunsn  12390  fprodcllem  12392  fprodabs  12402  fprodeq0  12403  fprodmodd  12427  eftlcvg  12473  negdvdsb  12593  dvdsnegb  12594  fsumdvds  12628  dvdsext  12641  addmodlteqALT  12645  nno  12692  gcdsupex  12753  gcdsupcl  12754  bezoutlembz  12800  dvdssq  12827  eucalgf  12852  dvdslcm  12866  lcmledvds  12867  lcmeq0  12868  lcmcl  12869  lcmdvds  12876  lcmgcdeq  12880  divgcdcoprmex  12899  isprm5lem  12939  phibndlem  13017  phiprmpw  13023  pc2dvds  13132  pcmpt  13145  prmpwdvds  13157  1arith  13169  4sqleminfi  13199  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsv  13305  ballotfilemsima  13311  ctiunctlemf  13381  ctiunct  13383  grpinva  13759  grprida  13760  sgrppropd  13781  mndpropd  13806  mhmpropd  13826  0mhm  13846  resmhm2  13848  resmhm2b  13849  grplcan  13920  mulgval  13978  mulgnn0z  14005  mulgnndir  14007  mulgnn0dir  14008  issubg2m  14045  issubg4m  14049  subgintm  14054  ghmf1  14129  resscntz  14160  cntzsgrpcl  14161  cntzsubm  14164  gzsummhm  14229  gsumressfi  14251  prdssgrpd  14275  prdsidlem  14277  prdsmndd  14278  srglmhm  14381  srgrmhm  14382  ringpropd  14427  crngpropd  14428  ringlghm  14450  ringrghm  14451  mulgass3  14475  issubrng2  14602  subrngpropd  14608  issubrg2  14633  subrgintm  14635  subrgpropd  14645  rhmpropd  14646  unitrrg  14660  lmodprop2d  14769  islss3  14800  lssintclm  14805  qusrhm  14949  issubassa3  15096  opnssneib  15348  neissex  15357  tgrest  15361  iscnp3  15395  cnpnei  15411  cnrest  15427  tx1cn  15461  txcnp  15463  elbl3ps  15586  elbl3  15587  blininf  15616  blssexps  15621  blssex  15622  blpnfctr  15631  mopni2  15675  blsscls2  15685  metss  15686  bdmet  15694  metrest  15698  metcn  15706  txmetcn  15711  bl2ioo  15742  ivthinclemlr  15829  ivthinclemur  15831  dvcj  15901  dvfre  15902  elplyd  15933  plyaddlem1  15939  plymullem1  15940  plymullem  15942  plycolemc  15950  plycjlemc  15952  coseq0q4123  16027  abssinper  16039  fsumdvdsmul  16251  ppiqub  16259  bposlem5  16281  lgsval2lem  16300  lgsval4lem  16301  lgsneg  16314  lgsmod  16316  lgsdir2  16323  lgsdir  16325  lgsne0  16328  lgssq  16330  lgsquadlem1  16367  usgredg2vlem2  16635  clwwlkccat  16813  clwwlknonex2lem2  16850  subctctexmid  17201  cvgcmp2n  17253  iswomninnlem  17271  nconstwlpo  17288