Theorem ad2ant2lr 761

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpteqb  7016  poseq  8163  omxpenlem  9076  fineqvlem  9236  marypha1lem  9403  fin23lem26  10327  axdc3lem4  10455  mulcmpblnr  11074  ltsrpr  11080  sub4  11521  muladd  11664  ltleadd  11715  divdivdiv  11934  divadddiv  11948  ltmul12a  12089  lt2mul2div  12111  xlemul1a  13332  fzrev  13634  facndiv  14344  fsumconst  15867  fprodconst  16058  isprm5  16791  acsfn2  17744  ghmeql  19340  subgdmdprd  20137  lssvacl  21101  lssvsubcl  21102  ocvin  21861  lindfmm  22014  sraassab  22055  scmatghm  22727  scmatmhm  22728  slesolinv  22874  slesolinvbi  22875  slesolex  22876  pm2mpf1lem  22988  pm2mpcoe1  22994  reftr  23708  alexsubALTlem2  24242  alexsubALTlem3  24243  blbas  24624  nmoco  24931  cncfmet  25105  cmetcaulem  25484  mbflimsup  25862  ulmdvlem3  26602  ptolemy  26698  ltssolem1  27876  madebdaylemlrcut  28129  3wlkdlem6  30553  vdn0conngrumgrv2  30584  frgrncvvdeqlem8  30694  frgrwopreglem5ALT  30710  grpoideu  30898  ipblnfi  31244  htthlem  31306  hvaddsub4  31467  bralnfn  32337  hmops  32409  hmopm  32410  adjadd  32482  opsqrlem1  32529  atomli  32771  chirredlem2  32780  atcvat3i  32785  mdsymlem5  32796  cdj1i  32822  derangenlem  35684  elmrsubrn  36033  dfon2lem6  36299  pibt2  38104  matunitlindflem1  38308  mblfinlem1  38349  prdsbnd  38485  heibor1lem  38501  hl2at  40220  congneg  43737  jm2.26  43770  stoweidlem34  46789  fmtnofac2lem  48361  lindslinindsimp2  49284  ltsubaddb  49335  ltsubadd2b  49337  aacllem  50662