Theorem ad2ant2lr 754

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpteqb  6962  poseq  8105  omxpenlem  9013  fineqvlem  9173  marypha1lem  9343  fin23lem26  10245  axdc3lem4  10373  mulcmpblnr  10992  ltsrpr  10998  sub4  11437  muladd  11580  ltleadd  11631  divdivdiv  11854  divadddiv  11868  ltmul12a  12009  lt2mul2div  12032  xlemul1a  13238  fzrev  13539  facndiv  14248  fsumconst  15750  fprodconst  15941  isprm5  16675  acsfn2  17627  ghmeql  19212  subgdmdprd  20009  lssvacl  20940  lssvsubcl  20941  ocvin  21656  lindfmm  21809  sraassab  21850  scmatghm  22523  scmatmhm  22524  slesolinv  22670  slesolinvbi  22671  slesolex  22672  pm2mpf1lem  22784  pm2mpcoe1  22790  reftr  23504  alexsubALTlem2  24038  alexsubALTlem3  24039  blbas  24420  nmoco  24727  cncfmet  24901  cmetcaulem  25280  mbflimsup  25658  ulmdvlem3  26392  ptolemy  26485  ltssolem1  27664  madebdaylemlrcut  27916  3wlkdlem6  30260  vdn0conngrumgrv2  30291  frgrncvvdeqlem8  30401  frgrwopreglem5ALT  30417  grpoideu  30605  ipblnfi  30951  htthlem  31013  hvaddsub4  31174  bralnfn  32044  hmops  32116  hmopm  32117  adjadd  32189  opsqrlem1  32236  atomli  32478  chirredlem2  32487  atcvat3i  32492  mdsymlem5  32503  cdj1i  32529  derangenlem  35406  elmrsubrn  35755  dfon2lem6  36021  pibt2  37786  matunitlindflem1  37990  mblfinlem1  38031  prdsbnd  38167  heibor1lem  38183  hl2at  39904  congneg  43421  jm2.26  43454  stoweidlem34  46484  fmtnofac2lem  48053  lindslinindsimp2  48961  ltsubaddb  49012  ltsubadd2b  49014  aacllem  50298