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 395

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 207  df-an 396

This theorem is referenced by:  mpteqb  7010  poseq  8162  omxpenlem  9092  fineqvlem  9275  marypha1lem  9450  fin23lem26  10344  axdc3lem4  10472  mulcmpblnr  11090  ltsrpr  11096  sub4  11533  muladd  11674  ltleadd  11725  divdivdiv  11947  divadddiv  11961  ltmul12a  12102  lt2mul2div  12125  xlemul1a  13309  fzrev  13609  facndiv  14311  fsumconst  15811  fprodconst  15999  isprm5  16731  acsfn2  17680  ghmeql  19227  subgdmdprd  20022  lssvacl  20905  lssvsubcl  20906  ocvin  21639  lindfmm  21792  sraassab  21833  scmatghm  22476  scmatmhm  22477  slesolinv  22623  slesolinvbi  22624  slesolex  22625  pm2mpf1lem  22737  pm2mpcoe1  22743  reftr  23457  alexsubALTlem2  23991  alexsubALTlem3  23992  blbas  24374  nmoco  24681  cncfmet  24858  cmetcaulem  25245  mbflimsup  25624  ulmdvlem3  26368  ptolemy  26462  sltsolem1  27644  madebdaylemlrcut  27867  3wlkdlem6  30151  vdn0conngrumgrv2  30182  frgrncvvdeqlem8  30292  frgrwopreglem5ALT  30308  grpoideu  30495  ipblnfi  30841  htthlem  30903  hvaddsub4  31064  bralnfn  31934  hmops  32006  hmopm  32007  adjadd  32079  opsqrlem1  32126  atomli  32368  chirredlem2  32377  atcvat3i  32382  mdsymlem5  32393  cdj1i  32419  derangenlem  35198  elmrsubrn  35547  dfon2lem6  35811  pibt2  37440  matunitlindflem1  37645  mblfinlem1  37686  prdsbnd  37822  heibor1lem  37838  hl2at  39429  congneg  42968  jm2.26  43001  stoweidlem34  46043  fmtnofac2lem  47562  lindslinindsimp2  48419  ltsubaddb  48470  ltsubadd2b  48472  aacllem  49645