Theorem ad2ant2lr 746

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 715	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 712	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpteqb  7020  poseq  8164  omxpenlem  9103  fineqvlem  9289  marypha1lem  9469  fin23lem26  10359  axdc3lem4  10487  mulcmpblnr  11105  ltsrpr  11111  sub4  11546  muladd  11687  ltleadd  11738  divdivdiv  11960  divadddiv  11974  ltmul12a  12115  lt2mul2div  12138  xlemul1a  13315  fzrev  13612  facndiv  14300  fsumconst  15789  fprodconst  15975  isprm5  16703  acsfn2  17671  ghmeql  19229  subgdmdprd  20030  lssvacl  20916  lssvsubcl  20917  ocvin  21666  lindfmm  21821  sraassab  21861  scmatghm  22523  scmatmhm  22524  slesolinv  22670  slesolinvbi  22671  slesolex  22672  pm2mpf1lem  22784  pm2mpcoe1  22790  reftr  23506  alexsubALTlem2  24040  alexsubALTlem3  24041  blbas  24424  nmoco  24742  cncfmet  24917  cmetcaulem  25304  mbflimsup  25683  ulmdvlem3  26428  ptolemy  26521  sltsolem1  27702  madebdaylemlrcut  27919  3wlkdlem6  30095  vdn0conngrumgrv2  30126  frgrncvvdeqlem8  30236  frgrwopreglem5ALT  30252  grpoideu  30439  ipblnfi  30785  htthlem  30847  hvaddsub4  31008  bralnfn  31878  hmops  31950  hmopm  31951  adjadd  32023  opsqrlem1  32070  atomli  32312  chirredlem2  32321  atcvat3i  32326  mdsymlem5  32337  cdj1i  32363  derangenlem  35012  elmrsubrn  35361  dfon2lem6  35625  pibt2  37137  matunitlindflem1  37330  mblfinlem1  37371  prdsbnd  37507  heibor1lem  37523  hl2at  39117  congneg  42664  jm2.26  42697  stoweidlem34  45691  fmtnofac2lem  47176  lindslinindsimp2  47882  ltsubaddb  47933  ltsubadd2b  47935  aacllem  48585