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  6953  poseq  8098  omxpenlem  9002  fineqvlem  9167  marypha1lem  9342  fin23lem26  10238  axdc3lem4  10366  mulcmpblnr  10984  ltsrpr  10990  sub4  11427  muladd  11570  ltleadd  11621  divdivdiv  11843  divadddiv  11857  ltmul12a  11998  lt2mul2div  12021  xlemul1a  13208  fzrev  13508  facndiv  14213  fsumconst  15715  fprodconst  15903  isprm5  16636  acsfn2  17587  ghmeql  19136  subgdmdprd  19933  lssvacl  20864  lssvsubcl  20865  ocvin  21599  lindfmm  21752  sraassab  21793  scmatghm  22436  scmatmhm  22437  slesolinv  22583  slesolinvbi  22584  slesolex  22585  pm2mpf1lem  22697  pm2mpcoe1  22703  reftr  23417  alexsubALTlem2  23951  alexsubALTlem3  23952  blbas  24334  nmoco  24641  cncfmet  24818  cmetcaulem  25204  mbflimsup  25583  ulmdvlem3  26327  ptolemy  26421  sltsolem1  27603  madebdaylemlrcut  27831  3wlkdlem6  30127  vdn0conngrumgrv2  30158  frgrncvvdeqlem8  30268  frgrwopreglem5ALT  30284  grpoideu  30471  ipblnfi  30817  htthlem  30879  hvaddsub4  31040  bralnfn  31910  hmops  31982  hmopm  31983  adjadd  32055  opsqrlem1  32102  atomli  32344  chirredlem2  32353  atcvat3i  32358  mdsymlem5  32369  cdj1i  32395  derangenlem  35146  elmrsubrn  35495  dfon2lem6  35764  pibt2  37393  matunitlindflem1  37598  mblfinlem1  37639  prdsbnd  37775  heibor1lem  37791  hl2at  39387  congneg  42945  jm2.26  42978  stoweidlem34  46019  fmtnofac2lem  47556  lindslinindsimp2  48452  ltsubaddb  48503  ltsubadd2b  48505  aacllem  49790