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  7011  poseq  8155  omxpenlem  9067  fineqvlem  9227  marypha1lem  9394  fin23lem26  10310  axdc3lem4  10438  mulcmpblnr  11057  ltsrpr  11063  sub4  11504  muladd  11647  ltleadd  11698  divdivdiv  11917  divadddiv  11931  ltmul12a  12072  lt2mul2div  12094  xlemul1a  13315  fzrev  13617  facndiv  14326  fsumconst  15843  fprodconst  16034  isprm5  16767  acsfn2  17720  ghmeql  19310  subgdmdprd  20107  lssvacl  21045  lssvsubcl  21046  ocvin  21805  lindfmm  21958  sraassab  21999  scmatghm  22671  scmatmhm  22672  slesolinv  22818  slesolinvbi  22819  slesolex  22820  pm2mpf1lem  22932  pm2mpcoe1  22938  reftr  23652  alexsubALTlem2  24186  alexsubALTlem3  24187  blbas  24568  nmoco  24875  cncfmet  25049  cmetcaulem  25428  mbflimsup  25806  ulmdvlem3  26546  ptolemy  26642  ltssolem1  27820  madebdaylemlrcut  28073  3wlkdlem6  30497  vdn0conngrumgrv2  30528  frgrncvvdeqlem8  30638  frgrwopreglem5ALT  30654  grpoideu  30842  ipblnfi  31188  htthlem  31250  hvaddsub4  31411  bralnfn  32281  hmops  32353  hmopm  32354  adjadd  32426  opsqrlem1  32473  atomli  32715  chirredlem2  32724  atcvat3i  32729  mdsymlem5  32740  cdj1i  32766  derangenlem  35644  elmrsubrn  35993  dfon2lem6  36259  pibt2  38044  matunitlindflem1  38248  mblfinlem1  38289  prdsbnd  38425  heibor1lem  38441  hl2at  40160  congneg  43679  jm2.26  43712  stoweidlem34  46731  fmtnofac2lem  48303  lindslinindsimp2  49226  ltsubaddb  49277  ltsubadd2b  49279  aacllem  50584