Theorem ad2ant2lr 760

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpteqb  6999  poseq  8142  omxpenlem  9054  fineqvlem  9214  marypha1lem  9381  fin23lem26  10297  axdc3lem4  10425  mulcmpblnr  11044  ltsrpr  11050  sub4  11491  muladd  11634  ltleadd  11685  divdivdiv  11904  divadddiv  11918  ltmul12a  12059  lt2mul2div  12081  xlemul1a  13302  fzrev  13603  facndiv  14312  fsumconst  15829  fprodconst  16020  isprm5  16754  acsfn2  17707  ghmeql  19297  subgdmdprd  20094  lssvacl  21030  lssvsubcl  21031  ocvin  21781  lindfmm  21934  sraassab  21975  scmatghm  22647  scmatmhm  22648  slesolinv  22794  slesolinvbi  22795  slesolex  22796  pm2mpf1lem  22908  pm2mpcoe1  22914  reftr  23628  alexsubALTlem2  24162  alexsubALTlem3  24163  blbas  24544  nmoco  24851  cncfmet  25025  cmetcaulem  25404  mbflimsup  25782  ulmdvlem3  26519  ptolemy  26615  ltssolem1  27793  madebdaylemlrcut  28046  3wlkdlem6  30421  vdn0conngrumgrv2  30452  frgrncvvdeqlem8  30562  frgrwopreglem5ALT  30578  grpoideu  30766  ipblnfi  31112  htthlem  31174  hvaddsub4  31335  bralnfn  32205  hmops  32277  hmopm  32278  adjadd  32350  opsqrlem1  32397  atomli  32639  chirredlem2  32648  atcvat3i  32653  mdsymlem5  32664  cdj1i  32690  derangenlem  35529  elmrsubrn  35878  dfon2lem6  36144  pibt2  37918  matunitlindflem1  38122  mblfinlem1  38163  prdsbnd  38299  heibor1lem  38315  hl2at  40036  congneg  43553  jm2.26  43586  stoweidlem34  46607  fmtnofac2lem  48176  lindslinindsimp2  49095  ltsubaddb  49146  ltsubadd2b  49148  aacllem  50431