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 395

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 207  df-an 396

This theorem is referenced by:  mpteqb  6960  poseq  8100  omxpenlem  9006  fineqvlem  9166  marypha1lem  9336  fin23lem26  10235  axdc3lem4  10363  mulcmpblnr  10982  ltsrpr  10988  sub4  11426  muladd  11569  ltleadd  11620  divdivdiv  11842  divadddiv  11856  ltmul12a  11997  lt2mul2div  12020  xlemul1a  13203  fzrev  13503  facndiv  14211  fsumconst  15713  fprodconst  15901  isprm5  16634  acsfn2  17586  ghmeql  19168  subgdmdprd  19965  lssvacl  20894  lssvsubcl  20895  ocvin  21629  lindfmm  21782  sraassab  21823  scmatghm  22477  scmatmhm  22478  slesolinv  22624  slesolinvbi  22625  slesolex  22626  pm2mpf1lem  22738  pm2mpcoe1  22744  reftr  23458  alexsubALTlem2  23992  alexsubALTlem3  23993  blbas  24374  nmoco  24681  cncfmet  24858  cmetcaulem  25244  mbflimsup  25623  ulmdvlem3  26367  ptolemy  26461  ltssolem1  27643  madebdaylemlrcut  27895  3wlkdlem6  30240  vdn0conngrumgrv2  30271  frgrncvvdeqlem8  30381  frgrwopreglem5ALT  30397  grpoideu  30584  ipblnfi  30930  htthlem  30992  hvaddsub4  31153  bralnfn  32023  hmops  32095  hmopm  32096  adjadd  32168  opsqrlem1  32215  atomli  32457  chirredlem2  32466  atcvat3i  32471  mdsymlem5  32482  cdj1i  32508  derangenlem  35365  elmrsubrn  35714  dfon2lem6  35980  pibt2  37622  matunitlindflem1  37817  mblfinlem1  37858  prdsbnd  37994  heibor1lem  38010  hl2at  39665  congneg  43211  jm2.26  43244  stoweidlem34  46278  fmtnofac2lem  47814  lindslinindsimp2  48709  ltsubaddb  48760  ltsubadd2b  48762  aacllem  50046