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  6956  poseq  8096  omxpenlem  9000  fineqvlem  9159  marypha1lem  9326  fin23lem26  10225  axdc3lem4  10353  mulcmpblnr  10971  ltsrpr  10977  sub4  11415  muladd  11558  ltleadd  11609  divdivdiv  11831  divadddiv  11845  ltmul12a  11986  lt2mul2div  12009  xlemul1a  13191  fzrev  13491  facndiv  14199  fsumconst  15701  fprodconst  15889  isprm5  16622  acsfn2  17573  ghmeql  19155  subgdmdprd  19952  lssvacl  20880  lssvsubcl  20881  ocvin  21615  lindfmm  21768  sraassab  21809  scmatghm  22451  scmatmhm  22452  slesolinv  22598  slesolinvbi  22599  slesolex  22600  pm2mpf1lem  22712  pm2mpcoe1  22718  reftr  23432  alexsubALTlem2  23966  alexsubALTlem3  23967  blbas  24348  nmoco  24655  cncfmet  24832  cmetcaulem  25218  mbflimsup  25597  ulmdvlem3  26341  ptolemy  26435  sltsolem1  27617  madebdaylemlrcut  27847  3wlkdlem6  30149  vdn0conngrumgrv2  30180  frgrncvvdeqlem8  30290  frgrwopreglem5ALT  30306  grpoideu  30493  ipblnfi  30839  htthlem  30901  hvaddsub4  31062  bralnfn  31932  hmops  32004  hmopm  32005  adjadd  32077  opsqrlem1  32124  atomli  32366  chirredlem2  32375  atcvat3i  32380  mdsymlem5  32391  cdj1i  32417  derangenlem  35238  elmrsubrn  35587  dfon2lem6  35853  pibt2  37484  matunitlindflem1  37679  mblfinlem1  37720  prdsbnd  37856  heibor1lem  37872  hl2at  39527  congneg  43089  jm2.26  43122  stoweidlem34  46159  fmtnofac2lem  47695  lindslinindsimp2  48591  ltsubaddb  48642  ltsubadd2b  48644  aacllem  49929