Theorem adantll 476

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

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		simpr 110	. 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:  ad2antlr  489  ad2ant2l  508  ad2ant2lr  510  ad5ant23  522  ad5ant24  523  ad5ant25  524  3ad2antl3  1185  3adant1l  1254  reu6  2993  sbc2iegf  3100  sbcralt  3106  sbcrext  3107  indifdir  3461  pofun  4407  poinxp  4793  ssimaex  5703  fndmdif  5748  dffo4  5791  fcompt  5813  fconst2g  5864  foco2  5889  foeqcnvco  5926  f1eqcocnv  5927  fliftel1  5930  isores3  5951  acexmid  6012  tfrlemi14d  6494  tfrcl  6525  dom2lem  6940  fiintim  7116  ordiso2  7225  mkvprop  7348  lt2addnq  7614  lt2mulnq  7615  ltexnqq  7618  genpdf  7718  addnqprl  7739  addnqpru  7740  addlocpr  7746  recexprlemopl  7835  caucvgsrlemgt1  8005  add4  8330  cnegex  8347  ltleadd  8616  zextle  9561  peano5uzti  9578  fnn0ind  9586  xrlttr  10020  xaddass  10094  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  fzaddel  10284  fzrev  10309  exbtwnzlemshrink  10498  xqltnle  10517  seq3val  10712  iseqf1olemab  10754  seqf1og  10773  exp3vallem  10792  mulexp  10830  expadd  10833  expmul  10836  leexp1a  10846  bccl  11019  hashfacen  11090  wrdnval  11134  swrdccat3blem  11310  ovshftex  11370  2shfti  11382  caucvgre  11532  cvg1nlemcau  11535  resqrexlemcvg  11570  cau3lem  11665  rexico  11772  iooinsup  11828  climmpt  11851  subcn2  11862  climrecvg1n  11899  climcvg1nlem  11900  climcaucn  11902  mertenslem2  12087  eftlcl  12239  reeftlcl  12240  dvdsext  12406  3dvds  12415  sqoddm1div8z  12437  bezoutlemaz  12564  bezoutr1  12594  dvdslcm  12631  lcmeq0  12633  lcmcl  12634  lcmneg  12636  lcmdvds  12641  coprmgcdb  12650  dvdsprime  12684  pc2dvds  12893  prmpwdvds  12918  infpnlem1  12922  1arith  12930  resmhm  13560  resmhm2b  13562  mhmco  13563  mhmima  13564  gsumwsubmcl  13569  dfgrp2  13600  mulgfng  13701  subgintm  13775  ghmmhmb  13831  resghm  13837  islmod  14295  islmodd  14297  cnco  14935  cnss1  14940  tx2cn  14984  upxp  14986  metss  15208  txmetcnp  15232  cncfss  15297  plyaddlem1  15461  plymullem1  15462  cosz12  15494  gausslemma2dlem4  15783  bj-findis  16510