Theorem ad2ant2lr 758

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpteqb  6989  poseq  8131  omxpenlem  9043  fineqvlem  9203  marypha1lem  9372  fin23lem26  10275  axdc3lem4  10403  mulcmpblnr  11022  ltsrpr  11028  sub4  11469  muladd  11612  ltleadd  11663  divdivdiv  11885  divadddiv  11899  ltmul12a  12040  lt2mul2div  12063  xlemul1a  13284  fzrev  13585  facndiv  14294  fsumconst  15807  fprodconst  15998  isprm5  16732  acsfn2  17685  ghmeql  19269  subgdmdprd  20066  lssvacl  20997  lssvsubcl  20998  ocvin  21713  lindfmm  21866  sraassab  21907  scmatghm  22580  scmatmhm  22581  slesolinv  22727  slesolinvbi  22728  slesolex  22729  pm2mpf1lem  22841  pm2mpcoe1  22847  reftr  23561  alexsubALTlem2  24095  alexsubALTlem3  24096  blbas  24477  nmoco  24784  cncfmet  24958  cmetcaulem  25337  mbflimsup  25715  ulmdvlem3  26452  ptolemy  26548  ltssolem1  27726  madebdaylemlrcut  27979  3wlkdlem6  30323  vdn0conngrumgrv2  30354  frgrncvvdeqlem8  30464  frgrwopreglem5ALT  30480  grpoideu  30668  ipblnfi  31014  htthlem  31076  hvaddsub4  31237  bralnfn  32107  hmops  32179  hmopm  32180  adjadd  32252  opsqrlem1  32299  atomli  32541  chirredlem2  32550  atcvat3i  32555  mdsymlem5  32566  cdj1i  32592  derangenlem  35481  elmrsubrn  35830  dfon2lem6  36096  pibt2  37871  matunitlindflem1  38075  mblfinlem1  38116  prdsbnd  38252  heibor1lem  38268  hl2at  39989  congneg  43506  jm2.26  43539  stoweidlem34  46568  fmtnofac2lem  48137  lindslinindsimp2  49045  ltsubaddb  49096  ltsubadd2b  49098  aacllem  50382