Theorem ad2ant2lr 799

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  reusv2lem2OLD  4900  mpteqb  6338  omxpenlem  8102  fineqvlem  8215  marypha1lem  8380  fin23lem26  9185  axdc3lem4  9313  mulcmpblnr  9930  ltsrpr  9936  sub4  10364  muladd  10500  ltleadd  10549  divdivdiv  10764  divadddiv  10778  ltmul12a  10917  lt2mul2div  10939  xlemul1a  12156  fzrev  12441  facndiv  13115  fsumconst  14566  fprodconst  14752  isprm5  15466  acsfn2  16371  ghmeql  17730  subgdmdprd  18479  lssvsubcl  18992  lssvacl  19002  ocvin  20066  lindfmm  20214  scmatghm  20387  scmatmhm  20388  slesolinv  20534  slesolinvbi  20535  slesolex  20536  pm2mpf1lem  20647  pm2mpcoe1  20653  reftr  21365  alexsubALTlem2  21899  alexsubALTlem3  21900  blbas  22282  nmoco  22588  cncfmet  22758  cmetcaulem  23132  mbflimsup  23478  ulmdvlem3  24201  ptolemy  24293  3wlkdlem6  27143  vdn0conngrumgrv2  27174  frgrncvvdeqlem8  27286  frgrwopreglem5ALT  27302  grpoideu  27491  ipblnfi  27839  htthlem  27902  hvaddsub4  28063  bralnfn  28935  hmops  29007  hmopm  29008  adjadd  29080  opsqrlem1  29127  atomli  29369  chirredlem2  29378  atcvat3i  29383  mdsymlem5  29394  cdj1i  29420  derangenlem  31279  elmrsubrn  31543  dfon2lem6  31817  poseq  31878  sltsolem1  31951  matunitlindflem1  33535  mblfinlem1  33576  prdsbnd  33722  heibor1lem  33738  hl2at  35009  congneg  37853  jm2.26  37886  stoweidlem34  40569  fmtnofac2lem  41805  lindslinindsimp2  42577  ltsubaddb  42629  ltsubadd2b  42631  aacllem  42875