Theorem ad2ant2lr 748

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2lr	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 717	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 714	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  mpteqb  6815  omxpenlem  8724  fineqvlem  8868  marypha1lem  9027  fin23lem26  9904  axdc3lem4  10032  mulcmpblnr  10650  ltsrpr  10656  sub4  11088  muladd  11229  ltleadd  11280  divdivdiv  11498  divadddiv  11512  ltmul12a  11653  lt2mul2div  11675  xlemul1a  12843  fzrev  13140  facndiv  13819  fsumconst  15317  fprodconst  15503  isprm5  16227  acsfn2  17120  ghmeql  18599  subgdmdprd  19375  lssvsubcl  19934  lssvacl  19945  ocvin  20590  lindfmm  20743  scmatghm  21384  scmatmhm  21385  slesolinv  21531  slesolinvbi  21532  slesolex  21533  pm2mpf1lem  21645  pm2mpcoe1  21651  reftr  22365  alexsubALTlem2  22899  alexsubALTlem3  22900  blbas  23282  nmoco  23589  cncfmet  23760  cmetcaulem  24139  mbflimsup  24517  ulmdvlem3  25248  ptolemy  25340  3wlkdlem6  28202  vdn0conngrumgrv2  28233  frgrncvvdeqlem8  28343  frgrwopreglem5ALT  28359  grpoideu  28544  ipblnfi  28890  htthlem  28952  hvaddsub4  29113  bralnfn  29983  hmops  30055  hmopm  30056  adjadd  30128  opsqrlem1  30175  atomli  30417  chirredlem2  30426  atcvat3i  30431  mdsymlem5  30442  cdj1i  30468  derangenlem  32800  elmrsubrn  33149  dfon2lem6  33434  poseq  33482  sltsolem1  33564  madebdaylemlrcut  33765  pibt2  35274  matunitlindflem1  35459  mblfinlem1  35500  prdsbnd  35637  heibor1lem  35653  hl2at  37105  congneg  40435  jm2.26  40468  stoweidlem34  43193  fmtnofac2lem  44636  lindslinindsimp2  45420  ltsubaddb  45471  ltsubadd2b  45473  aacllem  46119