Theorem ad2ant2lr 748

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 717	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 714	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  6771  omxpenlem  8631  fineqvlem  8746  marypha1lem  8915  fin23lem26  9770  axdc3lem4  9898  mulcmpblnr  10516  ltsrpr  10522  sub4  10954  muladd  11095  ltleadd  11146  divdivdiv  11364  divadddiv  11378  ltmul12a  11519  lt2mul2div  11541  xlemul1a  12707  fzrev  13004  facndiv  13683  fsumconst  15178  fprodconst  15365  isprm5  16088  acsfn2  16977  ghmeql  18433  subgdmdprd  19209  lssvsubcl  19768  lssvacl  19779  ocvin  20424  lindfmm  20577  scmatghm  21218  scmatmhm  21219  slesolinv  21365  slesolinvbi  21366  slesolex  21367  pm2mpf1lem  21479  pm2mpcoe1  21485  reftr  22199  alexsubALTlem2  22733  alexsubALTlem3  22734  blbas  23117  nmoco  23424  cncfmet  23595  cmetcaulem  23973  mbflimsup  24351  ulmdvlem3  25081  ptolemy  25173  3wlkdlem6  28034  vdn0conngrumgrv2  28065  frgrncvvdeqlem8  28175  frgrwopreglem5ALT  28191  grpoideu  28376  ipblnfi  28722  htthlem  28784  hvaddsub4  28945  bralnfn  29815  hmops  29887  hmopm  29888  adjadd  29960  opsqrlem1  30007  atomli  30249  chirredlem2  30258  atcvat3i  30263  mdsymlem5  30274  cdj1i  30300  derangenlem  32634  elmrsubrn  32983  dfon2lem6  33265  poseq  33341  sltsolem1  33428  madebdaylemlrcut  33621  pibt2  35099  matunitlindflem1  35318  mblfinlem1  35359  prdsbnd  35496  heibor1lem  35512  hl2at  36966  congneg  40268  jm2.26  40301  stoweidlem34  43027  fmtnofac2lem  44438  lindslinindsimp2  45222  ltsubaddb  45273  ltsubadd2b  45275  aacllem  45679