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  7035  poseq  8182  omxpenlem  9112  fineqvlem  9296  marypha1lem  9471  fin23lem26  10363  axdc3lem4  10491  mulcmpblnr  11109  ltsrpr  11115  sub4  11552  muladd  11693  ltleadd  11744  divdivdiv  11966  divadddiv  11980  ltmul12a  12121  lt2mul2div  12144  xlemul1a  13327  fzrev  13624  facndiv  14324  fsumconst  15823  fprodconst  16011  isprm5  16741  acsfn2  17708  ghmeql  19270  subgdmdprd  20069  lssvacl  20959  lssvsubcl  20960  ocvin  21710  lindfmm  21865  sraassab  21906  scmatghm  22555  scmatmhm  22556  slesolinv  22702  slesolinvbi  22703  slesolex  22704  pm2mpf1lem  22816  pm2mpcoe1  22822  reftr  23538  alexsubALTlem2  24072  alexsubALTlem3  24073  blbas  24456  nmoco  24774  cncfmet  24949  cmetcaulem  25336  mbflimsup  25715  ulmdvlem3  26460  ptolemy  26553  sltsolem1  27735  madebdaylemlrcut  27952  3wlkdlem6  30194  vdn0conngrumgrv2  30225  frgrncvvdeqlem8  30335  frgrwopreglem5ALT  30351  grpoideu  30538  ipblnfi  30884  htthlem  30946  hvaddsub4  31107  bralnfn  31977  hmops  32049  hmopm  32050  adjadd  32122  opsqrlem1  32169  atomli  32411  chirredlem2  32420  atcvat3i  32425  mdsymlem5  32436  cdj1i  32462  derangenlem  35156  elmrsubrn  35505  dfon2lem6  35770  pibt2  37400  matunitlindflem1  37603  mblfinlem1  37644  prdsbnd  37780  heibor1lem  37796  hl2at  39388  congneg  42958  jm2.26  42991  stoweidlem34  45990  fmtnofac2lem  47493  lindslinindsimp2  48309  ltsubaddb  48360  ltsubadd2b  48362  aacllem  49032