Theorem ad2ant2lr 735

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpteqb  6613  omxpenlem  8414  fineqvlem  8527  marypha1lem  8692  fin23lem26  9545  axdc3lem4  9673  mulcmpblnr  10291  ltsrpr  10297  sub4  10732  muladd  10873  ltleadd  10924  divdivdiv  11142  divadddiv  11156  ltmul12a  11297  lt2mul2div  11319  xlemul1a  12497  fzrev  12786  facndiv  13463  fsumconst  15005  fprodconst  15192  isprm5  15907  acsfn2  16792  ghmeql  18152  subgdmdprd  18906  lssvsubcl  19437  lssvacl  19448  ocvin  20520  lindfmm  20673  scmatghm  20846  scmatmhm  20847  slesolinv  20993  slesolinvbi  20994  slesolex  20995  pm2mpf1lem  21106  pm2mpcoe1  21112  reftr  21826  alexsubALTlem2  22360  alexsubALTlem3  22361  blbas  22743  nmoco  23049  cncfmet  23219  cmetcaulem  23594  mbflimsup  23970  ulmdvlem3  24693  ptolemy  24785  3wlkdlem6  27694  vdn0conngrumgrv2  27725  frgrncvvdeqlem8  27840  frgrwopreglem5ALT  27856  grpoideu  28063  ipblnfi  28410  htthlem  28473  hvaddsub4  28634  bralnfn  29506  hmops  29578  hmopm  29579  adjadd  29651  opsqrlem1  29698  atomli  29940  chirredlem2  29949  atcvat3i  29954  mdsymlem5  29965  cdj1i  29991  derangenlem  32009  elmrsubrn  32293  dfon2lem6  32559  poseq  32622  sltsolem1  32707  pibt2  34145  matunitlindflem1  34335  mblfinlem1  34376  prdsbnd  34519  heibor1lem  34535  hl2at  35992  congneg  38968  jm2.26  39001  stoweidlem34  41756  fmtnofac2lem  43104  lindslinindsimp2  43891  ltsubaddb  43943  ltsubadd2b  43945  aacllem  44275