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  1159  3ad2antl2  1160  ad4ant124  1216  3adant1r  1231  bilukdc  1396  intab  3874  pofun  4313  ralxfrd  4463  rexxfrd  4464  ordtri2or2exmidlem  4526  wessep  4578  poinxp  4696  relop  4778  fun11iun  5483  ssimaex  5578  fndmdif  5622  fconst2g  5732  foeqcnvco  5791  f1eqcocnv  5792  isocnv  5812  isocnv2  5813  riota2df  5851  f1o2ndf1  6229  tfr1onlembacc  6343  tfr1onlemaccex  6349  tfr1onlemres  6350  tfrcllembacc  6356  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  tfrcl  6365  xpdom2  6831  fimax2gtrilemstep  6900  xpfi  6929  eqsupti  6995  ordiso2  7034  enumctlemm  7113  enwomnilem  7167  cc2lem  7265  mulcanpig  7334  prarloclemlt  7492  genpdf  7507  genpdisj  7522  addnqprl  7528  addnqpru  7529  addlocpr  7535  prmuloc  7565  mulnqprl  7567  mulnqpru  7568  mullocpr  7570  ltpopr  7594  ltsopr  7595  ltaddpr  7596  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  ltaprg  7618  recexprlemopu  7626  recexprlemloc  7630  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  suplocsrlem  7807  axcaucvglemcau  7897  axpre-suploclemres  7900  axsuploc  8030  cnegexlem1  8132  cnegexlem3  8134  cnegex  8135  addsubeq4  8172  rimul  8542  divcanap6  8676  ltmul12a  8817  lemul12b  8818  lbinf  8905  zrevaddcl  9303  nzadd  9305  zextle  9344  fzind  9368  uz11  9550  infregelbex  9598  qreccl  9642  qrevaddcl  9644  irradd  9646  xrlttr  9795  xrltso  9796  xaddass  9869  xleadd1a  9873  xlt2add  9880  iccshftr  9994  iccshftl  9996  iccdil  9998  icccntr  10000  divelunit  10002  uzsubsubfz  10047  fzaddel  10059  fzrev  10084  elfzmlbp  10132  frec2uzrdg  10409  frecuzrdgtcl  10412  frecuzrdgsuc  10414  frecuzrdgdomlem  10417  frecuzrdgfunlem  10419  frecuzrdgsuctlem  10423  iseqovex  10456  seq3val  10458  seqf  10461  seq3clss  10467  seq3fveq2  10469  seq3feq2  10470  seq3feq  10472  seq3shft2  10473  ser3mono  10478  seq3split  10479  seq3caopr3  10481  seq3caopr2  10482  iseqf1olemab  10489  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1olemstep  10501  seq3f1oleml  10503  seq3id3  10507  seq3id  10508  seq3id2  10509  seq3homo  10510  seq3z  10511  seqfeq3  10512  ser3ge0  10517  expp1  10527  expnegap0  10528  expcllem  10531  mulexp  10559  expadd  10562  expaddzap  10564  expmulzap  10566  expdivap  10571  leexp1a  10575  expnlbnd  10645  bcpasc  10746  bccl  10747  hashfacen  10816  seq3coll  10822  seq3shft  10847  resqrexlemfp1  11018  sqrtdiv  11051  climshftlemg  11310  climcn1  11316  climsqz  11343  climsqz2  11344  clim2ser  11345  clim2ser2  11346  isermulc2  11348  climub  11352  serf0  11360  fsum3cvg  11386  sumrbdc  11387  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumf1o  11398  isumss  11399  fisumss  11400  isumss2  11401  fsum3cvg2  11402  fsum3cvg3  11404  fsumcl2lem  11406  fsumcllem  11407  fsumadd  11414  fsumsplit  11415  fsumsplitsn  11418  sumsplitdc  11440  fisumrev2  11454  fsum2mul  11461  fsum00  11470  telfsumo  11474  fsumparts  11478  iserabs  11483  cvgratnnlemabsle  11535  cvgratnn  11539  cvgratz  11540  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  clim2prod  11547  clim2divap  11548  prodfap0  11553  prodfrecap  11554  prodeq2  11565  fproddccvg  11580  prodrbdclem2  11581  prodmodc  11586  zproddc  11587  fprodf1o  11596  fprodssdc  11598  fprodunsn  11612  fprodcllem  11614  fprodabs  11624  fprodeq0  11625  fprodmodd  11649  eftlcvg  11695  negdvdsb  11814  dvdsnegb  11815  dvdsext  11861  addmodlteqALT  11865  nno  11911  infssuzex  11950  zsupssdc  11955  gcdsupex  11958  gcdsupcl  11959  bezoutlembz  12005  dvdssq  12032  eucalgf  12055  dvdslcm  12069  lcmledvds  12070  lcmeq0  12071  lcmcl  12072  lcmdvds  12079  lcmgcdeq  12083  divgcdcoprmex  12102  isprm5lem  12141  phibndlem  12216  phiprmpw  12222  pc2dvds  12329  pcmpt  12341  prmpwdvds  12353  1arith  12365  ctiunctlemf  12439  ctiunct  12441  grprinvd  12805  grpridd  12806  mndpropd  12841  mhmpropd  12857  0mhm  12873  grplcan  12932  mulgval  12986  mulgnn0z  13010  mulgnndir  13012  mulgnn0dir  13013  issubg2m  13049  issubg4m  13053  subgintm  13058  srglmhm  13176  srgrmhm  13177  ringpropd  13217  crngpropd  13218  mulgass3  13254  issubrg2  13362  subrgintm  13364  subrgpropd  13369  lmodprop2d  13438  opnssneib  13659  neissex  13668  tgrest  13672  iscnp3  13706  cnpnei  13722  cnrest  13738  tx1cn  13772  txcnp  13774  elbl3ps  13897  elbl3  13898  blininf  13927  blssexps  13932  blssex  13933  blpnfctr  13942  mopni2  13986  blsscls2  13996  metss  13997  bdmet  14005  metrest  14009  metcn  14017  txmetcn  14022  bl2ioo  14045  ivthinclemlr  14118  ivthinclemur  14120  dvcj  14176  dvfre  14177  coseq0q4123  14258  abssinper  14270  lgsval2lem  14414  lgsval4lem  14415  lgsneg  14428  lgsmod  14430  lgsdir2  14437  lgsdir  14439  lgsne0  14442  lgssq  14444  subctctexmid  14753  cvgcmp2n  14784  iswomninnlem  14800  nconstwlpo  14816