Theorem ad2ant2lr 745

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 714	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 711	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpteqb  6951  poseq  8046  omxpenlem  8939  fineqvlem  9128  marypha1lem  9291  fin23lem26  10183  axdc3lem4  10311  mulcmpblnr  10929  ltsrpr  10935  sub4  11368  muladd  11509  ltleadd  11560  divdivdiv  11778  divadddiv  11792  ltmul12a  11933  lt2mul2div  11955  xlemul1a  13124  fzrev  13421  facndiv  14104  fsumconst  15602  fprodconst  15788  isprm5  16510  acsfn2  17470  ghmeql  18954  subgdmdprd  19733  lssvsubcl  20312  lssvacl  20323  ocvin  20986  lindfmm  21141  scmatghm  21789  scmatmhm  21790  slesolinv  21936  slesolinvbi  21937  slesolex  21938  pm2mpf1lem  22050  pm2mpcoe1  22056  reftr  22772  alexsubALTlem2  23306  alexsubALTlem3  23307  blbas  23690  nmoco  24008  cncfmet  24179  cmetcaulem  24559  mbflimsup  24937  ulmdvlem3  25668  ptolemy  25760  sltsolem1  26930  3wlkdlem6  28818  vdn0conngrumgrv2  28849  frgrncvvdeqlem8  28959  frgrwopreglem5ALT  28975  grpoideu  29160  ipblnfi  29506  htthlem  29568  hvaddsub4  29729  bralnfn  30599  hmops  30671  hmopm  30672  adjadd  30744  opsqrlem1  30791  atomli  31033  chirredlem2  31042  atcvat3i  31047  mdsymlem5  31058  cdj1i  31084  derangenlem  33432  elmrsubrn  33781  dfon2lem6  34049  madebdaylemlrcut  34189  pibt2  35744  matunitlindflem1  35929  mblfinlem1  35970  prdsbnd  36107  heibor1lem  36123  hl2at  37724  congneg  41105  jm2.26  41138  stoweidlem34  43963  fmtnofac2lem  45438  lindslinindsimp2  46222  ltsubaddb  46273  ltsubadd2b  46275  aacllem  46923