Theorem ad2ant2lr 744

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 713	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 710	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  7016  poseq  8146  omxpenlem  9075  fineqvlem  9264  marypha1lem  9430  fin23lem26  10322  axdc3lem4  10450  mulcmpblnr  11068  ltsrpr  11074  sub4  11509  muladd  11650  ltleadd  11701  divdivdiv  11919  divadddiv  11933  ltmul12a  12074  lt2mul2div  12096  xlemul1a  13271  fzrev  13568  facndiv  14252  fsumconst  15740  fprodconst  15926  isprm5  16648  acsfn2  17611  ghmeql  19153  subgdmdprd  19945  lssvsubcl  20698  lssvacl  20709  ocvin  21446  lindfmm  21601  sraassab  21641  scmatghm  22255  scmatmhm  22256  slesolinv  22402  slesolinvbi  22403  slesolex  22404  pm2mpf1lem  22516  pm2mpcoe1  22522  reftr  23238  alexsubALTlem2  23772  alexsubALTlem3  23773  blbas  24156  nmoco  24474  cncfmet  24649  cmetcaulem  25036  mbflimsup  25415  ulmdvlem3  26150  ptolemy  26242  sltsolem1  27414  madebdaylemlrcut  27630  3wlkdlem6  29685  vdn0conngrumgrv2  29716  frgrncvvdeqlem8  29826  frgrwopreglem5ALT  29842  grpoideu  30029  ipblnfi  30375  htthlem  30437  hvaddsub4  30598  bralnfn  31468  hmops  31540  hmopm  31541  adjadd  31613  opsqrlem1  31660  atomli  31902  chirredlem2  31911  atcvat3i  31916  mdsymlem5  31927  cdj1i  31953  derangenlem  34460  elmrsubrn  34809  dfon2lem6  35064  pibt2  36601  matunitlindflem1  36787  mblfinlem1  36828  prdsbnd  36964  heibor1lem  36980  hl2at  38579  congneg  42010  jm2.26  42043  stoweidlem34  45048  fmtnofac2lem  46534  lindslinindsimp2  47231  ltsubaddb  47282  ltsubadd2b  47284  aacllem  47935