Theorem adantlr 466

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 108	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 279	1 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antrr  477  ad2ant2r  498  ad2ant2rl  500  3ad2antl1  1124  3ad2antl2  1125  ad4ant124  1175  3adant1r  1190  bilukdc  1355  intab  3764  pofun  4192  ralxfrd  4341  rexxfrd  4342  ordtri2or2exmidlem  4399  wessep  4450  poinxp  4566  relop  4647  fun11iun  5342  ssimaex  5434  fndmdif  5477  fconst2g  5587  foeqcnvco  5643  f1eqcocnv  5644  isocnv  5664  isocnv2  5665  riota2df  5702  grprinvd  5918  grpridd  5919  f1o2ndf1  6077  tfr1onlembacc  6191  tfr1onlemaccex  6197  tfr1onlemres  6198  tfrcllembacc  6204  tfrcllemaccex  6210  tfrcllemres  6211  tfrcldm  6212  tfrcl  6213  xpdom2  6676  fimax2gtrilemstep  6745  xpfi  6769  eqsupti  6833  ordiso2  6870  enumctlemm  6949  mulcanpig  7085  prarloclemlt  7243  genpdf  7258  genpdisj  7273  addnqprl  7279  addnqpru  7280  addlocpr  7286  prmuloc  7316  mulnqprl  7318  mulnqpru  7319  mullocpr  7321  ltpopr  7345  ltsopr  7346  ltaddpr  7347  ltexprlemdisj  7356  ltexprlemloc  7357  ltexprlemru  7362  addcanprleml  7364  addcanprlemu  7365  ltaprg  7369  recexprlemopu  7377  recexprlemloc  7381  cauappcvgprlemladdfl  7405  cauappcvgprlemladdru  7406  caucvgsrlemcau  7529  caucvgsrlemgt1  7531  caucvgsrlemoffcau  7534  caucvgsrlemoffres  7536  axcaucvglemcau  7627  cnegexlem1  7854  cnegexlem3  7856  cnegex  7857  addsubeq4  7894  rimul  8259  divcanap6  8386  ltmul12a  8522  lemul12b  8523  lbinf  8610  zrevaddcl  9002  nzadd  9004  zextle  9040  fzind  9064  uz11  9244  qreccl  9330  qrevaddcl  9332  irradd  9334  xrlttr  9468  xrltso  9469  xaddass  9539  xleadd1a  9543  xlt2add  9550  iccshftr  9664  iccshftl  9666  iccdil  9668  icccntr  9670  divelunit  9672  uzsubsubfz  9714  fzaddel  9726  fzrev  9751  elfzmlbp  9796  frec2uzrdg  10069  frecuzrdgtcl  10072  frecuzrdgsuc  10074  frecuzrdgdomlem  10077  frecuzrdgfunlem  10079  frecuzrdgsuctlem  10083  iseqovex  10116  seq3val  10118  seqf  10121  seq3clss  10127  seq3fveq2  10129  seq3feq2  10130  seq3feq  10132  seq3shft2  10133  ser3mono  10138  seq3split  10139  seq3caopr3  10141  seq3caopr2  10142  iseqf1olemab  10149  seq3f1olemqsumkj  10158  seq3f1olemqsumk  10159  seq3f1olemqsum  10160  seq3f1olemstep  10161  seq3f1oleml  10163  seq3id3  10167  seq3id  10168  seq3id2  10169  seq3homo  10170  seq3z  10171  seqfeq3  10172  ser3ge0  10177  expp1  10187  expnegap0  10188  expcllem  10191  mulexp  10219  expadd  10222  expaddzap  10224  expmulzap  10226  expdivap  10231  leexp1a  10235  expnlbnd  10303  bcpasc  10399  bccl  10400  hashfacen  10466  seq3coll  10472  seq3shft  10497  resqrexlemfp1  10667  sqrtdiv  10700  climshftlemg  10957  climcn1  10963  climsqz  10990  climsqz2  10991  clim2ser  10992  clim2ser2  10993  isermulc2  10995  climub  10999  serf0  11007  fsum3cvg  11032  sumrbdc  11033  summodclem3  11035  summodclem2a  11036  zsumdc  11039  fsumf1o  11045  isumss  11046  fisumss  11047  isumss2  11048  fsum3cvg2  11049  fsum3cvg3  11051  fsumcl2lem  11053  fsumcllem  11054  fsumadd  11061  fsumsplit  11062  fsumsplitsn  11065  sumsplitdc  11087  fisumrev2  11101  fsum2mul  11108  fsum00  11117  telfsumo  11121  fsumparts  11125  iserabs  11130  cvgratnnlemabsle  11182  cvgratnn  11186  cvgratz  11187  mertenslemub  11189  mertenslemi1  11190  mertenslem2  11191  mertensabs  11192  eftlcvg  11238  negdvdsb  11351  dvdsnegb  11352  dvdsext  11395  addmodlteqALT  11399  nno  11445  infssuzex  11484  gcdsupex  11488  gcdsupcl  11489  bezoutlembz  11532  dvdssq  11559  eucalgf  11576  dvdslcm  11590  lcmledvds  11591  lcmeq0  11592  lcmcl  11593  lcmdvds  11600  lcmgcdeq  11604  divgcdcoprmex  11623  phibndlem  11731  phiprmpw  11737  ctiunctlemf  11788  ctiunct  11790  opnssneib  12162  neissex  12171  tgrest  12175  iscnp3  12208  cnpnei  12224  cnrest  12240  tx1cn  12274  txcnp  12276  elbl3ps  12377  elbl3  12378  blininf  12407  blssexps  12412  blssex  12413  blpnfctr  12422  mopni2  12466  blsscls2  12476  metss  12477  bdmet  12485  metrest  12489  metcn  12497  txmetcn  12502  bl2ioo  12522  cvgcmp2n  12909