Theorem ad2ant2lr 747

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 716	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 713	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  7048  poseq  8199  omxpenlem  9139  fineqvlem  9325  marypha1lem  9502  fin23lem26  10394  axdc3lem4  10522  mulcmpblnr  11140  ltsrpr  11146  sub4  11581  muladd  11722  ltleadd  11773  divdivdiv  11995  divadddiv  12009  ltmul12a  12150  lt2mul2div  12173  xlemul1a  13350  fzrev  13647  facndiv  14337  fsumconst  15838  fprodconst  16026  isprm5  16754  acsfn2  17721  ghmeql  19279  subgdmdprd  20078  lssvacl  20964  lssvsubcl  20965  ocvin  21715  lindfmm  21870  sraassab  21911  scmatghm  22560  scmatmhm  22561  slesolinv  22707  slesolinvbi  22708  slesolex  22709  pm2mpf1lem  22821  pm2mpcoe1  22827  reftr  23543  alexsubALTlem2  24077  alexsubALTlem3  24078  blbas  24461  nmoco  24779  cncfmet  24954  cmetcaulem  25341  mbflimsup  25720  ulmdvlem3  26463  ptolemy  26556  sltsolem1  27738  madebdaylemlrcut  27955  3wlkdlem6  30197  vdn0conngrumgrv2  30228  frgrncvvdeqlem8  30338  frgrwopreglem5ALT  30354  grpoideu  30541  ipblnfi  30887  htthlem  30949  hvaddsub4  31110  bralnfn  31980  hmops  32052  hmopm  32053  adjadd  32125  opsqrlem1  32172  atomli  32414  chirredlem2  32423  atcvat3i  32428  mdsymlem5  32439  cdj1i  32465  derangenlem  35139  elmrsubrn  35488  dfon2lem6  35752  pibt2  37383  matunitlindflem1  37576  mblfinlem1  37617  prdsbnd  37753  heibor1lem  37769  hl2at  39362  congneg  42926  jm2.26  42959  stoweidlem34  45955  fmtnofac2lem  47442  lindslinindsimp2  48192  ltsubaddb  48243  ltsubadd2b  48245  aacllem  48895