Theorem ad2ant2lr 749

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 718	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 715	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  6961  poseq  8101  omxpenlem  9009  fineqvlem  9169  marypha1lem  9339  fin23lem26  10238  axdc3lem4  10366  mulcmpblnr  10985  ltsrpr  10991  sub4  11430  muladd  11573  ltleadd  11624  divdivdiv  11847  divadddiv  11861  ltmul12a  12002  lt2mul2div  12025  xlemul1a  13231  fzrev  13532  facndiv  14241  fsumconst  15743  fprodconst  15934  isprm5  16668  acsfn2  17620  ghmeql  19205  subgdmdprd  20002  lssvacl  20929  lssvsubcl  20930  ocvin  21664  lindfmm  21817  sraassab  21858  scmatghm  22508  scmatmhm  22509  slesolinv  22655  slesolinvbi  22656  slesolex  22657  pm2mpf1lem  22769  pm2mpcoe1  22775  reftr  23489  alexsubALTlem2  24023  alexsubALTlem3  24024  blbas  24405  nmoco  24712  cncfmet  24886  cmetcaulem  25265  mbflimsup  25643  ulmdvlem3  26380  ptolemy  26473  ltssolem1  27653  madebdaylemlrcut  27905  3wlkdlem6  30250  vdn0conngrumgrv2  30281  frgrncvvdeqlem8  30391  frgrwopreglem5ALT  30407  grpoideu  30595  ipblnfi  30941  htthlem  31003  hvaddsub4  31164  bralnfn  32034  hmops  32106  hmopm  32107  adjadd  32179  opsqrlem1  32226  atomli  32468  chirredlem2  32477  atcvat3i  32482  mdsymlem5  32493  cdj1i  32519  derangenlem  35369  elmrsubrn  35718  dfon2lem6  35984  pibt2  37747  matunitlindflem1  37951  mblfinlem1  37992  prdsbnd  38128  heibor1lem  38144  hl2at  39865  congneg  43415  jm2.26  43448  stoweidlem34  46480  fmtnofac2lem  48043  lindslinindsimp2  48951  ltsubaddb  49002  ltsubadd2b  49004  aacllem  50288