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  7039  poseq  8205  omxpenlem  9128  fineqvlem  9288  marypha1lem  9455  fin23lem26  10433  axdc3lem4  10561  mulcmpblnr  11186  ltsrpr  11192  sub4  11633  muladd  11778  ltleadd  11829  divdivdiv  12048  divadddiv  12062  ltmul12a  12203  lt2mul2div  12225  xlemul1a  13448  fzrev  13751  facndiv  14462  fsumconst  15988  fprodconst  16177  isprm5  16915  acsfn2  17869  ghmeql  19485  subgdmdprd  20283  lssvacl  21251  lssvsubcl  21252  ocvin  22013  lindfmm  22166  sraassab  22209  scmatghm  22881  scmatmhm  22882  matunitlindflem1  23027  slesolinv  23031  slesolinvbi  23032  slesolex  23033  pm2mpf1lem  23145  pm2mpcoe1  23151  reftr  23866  alexsubALTlem2  24400  alexsubALTlem3  24401  blbas  24782  nmoco  25089  cncfmet  25263  cmetcaulem  25642  mbflimsup  26020  ulmdvlem3  26762  ptolemy  26858  ltssolem1  28065  madebdaylemlrcut  28318  3wlkdlem6  30799  vdn0conngrumgrv2  30830  frgrncvvdeqlem8  30940  frgrwopreglem5ALT  30956  grpoideu  31144  ipblnfi  31490  htthlem  31552  hvaddsub4  31713  bralnfn  32583  hmops  32655  hmopm  32656  adjadd  32728  opsqrlem1  32775  atomli  33017  chirredlem2  33026  atcvat3i  33031  mdsymlem5  33042  cdj1i  33068  derangenlem  36116  elmrsubrn  36465  dfon2lem6  36741  pibt2  38545  mblfinlem1  38780  prdsbnd  38930  heibor1lem  38946  hl2at  40665  congneg  44180  jm2.26  44213  stoweidlem34  47259  fmtnofac2lem  48868  lindslinindsimp2  49790  ltsubaddb  49841  ltsubadd2b  49843  aacllem  51251