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  7005  poseq  8159  omxpenlem  9081  fineqvlem  9241  marypha1lem  9409  fin23lem26  10384  axdc3lem4  10512  mulcmpblnr  11137  ltsrpr  11143  sub4  11584  muladd  11729  ltleadd  11780  divdivdiv  11999  divadddiv  12013  ltmul12a  12154  lt2mul2div  12176  xlemul1a  13399  fzrev  13701  facndiv  14412  fsumconst  15936  fprodconst  16125  isprm5  16863  acsfn2  17817  ghmeql  19433  subgdmdprd  20230  lssvacl  21198  lssvsubcl  21199  ocvin  21960  lindfmm  22113  sraassab  22156  scmatghm  22828  scmatmhm  22829  matunitlindflem1  22974  slesolinv  22978  slesolinvbi  22979  slesolex  22980  pm2mpf1lem  23092  pm2mpcoe1  23098  reftr  23813  alexsubALTlem2  24347  alexsubALTlem3  24348  blbas  24729  nmoco  25036  cncfmet  25210  cmetcaulem  25589  mbflimsup  25967  ulmdvlem3  26711  ptolemy  26807  ltssolem1  28014  madebdaylemlrcut  28267  3wlkdlem6  30748  vdn0conngrumgrv2  30779  frgrncvvdeqlem8  30889  frgrwopreglem5ALT  30905  grpoideu  31093  ipblnfi  31439  htthlem  31501  hvaddsub4  31662  bralnfn  32532  hmops  32604  hmopm  32605  adjadd  32677  opsqrlem1  32724  atomli  32966  chirredlem2  32975  atcvat3i  32980  mdsymlem5  32991  cdj1i  33017  derangenlem  35905  elmrsubrn  36254  dfon2lem6  36520  pibt2  38308  mblfinlem1  38543  prdsbnd  38695  heibor1lem  38711  hl2at  40430  congneg  43929  jm2.26  43962  stoweidlem34  46988  fmtnofac2lem  48597  lindslinindsimp2  49519  ltsubaddb  49570  ltsubadd2b  49572  aacllem  50883