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  7010  poseq  8160  omxpenlem  9080  fineqvlem  9240  marypha1lem  9407  fin23lem26  10331  axdc3lem4  10459  mulcmpblnr  11084  ltsrpr  11090  sub4  11531  muladd  11674  ltleadd  11725  divdivdiv  11944  divadddiv  11958  ltmul12a  12099  lt2mul2div  12121  xlemul1a  13344  fzrev  13646  facndiv  14356  fsumconst  15880  fprodconst  16071  isprm5  16804  acsfn2  17757  ghmeql  19372  subgdmdprd  20169  lssvacl  21133  lssvsubcl  21134  ocvin  21893  lindfmm  22046  sraassab  22089  scmatghm  22761  scmatmhm  22762  matunitlindflem1  22907  slesolinv  22911  slesolinvbi  22912  slesolex  22913  pm2mpf1lem  23025  pm2mpcoe1  23031  reftr  23746  alexsubALTlem2  24280  alexsubALTlem3  24281  blbas  24662  nmoco  24969  cncfmet  25143  cmetcaulem  25522  mbflimsup  25900  ulmdvlem3  26645  ptolemy  26741  ltssolem1  27919  madebdaylemlrcut  28172  3wlkdlem6  30653  vdn0conngrumgrv2  30684  frgrncvvdeqlem8  30794  frgrwopreglem5ALT  30810  grpoideu  30998  ipblnfi  31344  htthlem  31406  hvaddsub4  31567  bralnfn  32437  hmops  32509  hmopm  32510  adjadd  32582  opsqrlem1  32629  atomli  32871  chirredlem2  32880  atcvat3i  32885  mdsymlem5  32896  cdj1i  32922  derangenlem  35758  elmrsubrn  36107  dfon2lem6  36373  pibt2  38179  mblfinlem1  38414  prdsbnd  38551  heibor1lem  38567  hl2at  40286  congneg  43818  jm2.26  43851  stoweidlem34  46870  fmtnofac2lem  48479  lindslinindsimp2  49401  ltsubaddb  49452  ltsubadd2b  49454  aacllem  50780