Theorem ad2ant2lr 747

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpteqb  7018  poseq  8144  omxpenlem  9073  fineqvlem  9262  marypha1lem  9428  fin23lem26  10320  axdc3lem4  10448  mulcmpblnr  11066  ltsrpr  11072  sub4  11505  muladd  11646  ltleadd  11697  divdivdiv  11915  divadddiv  11929  ltmul12a  12070  lt2mul2div  12092  xlemul1a  13267  fzrev  13564  facndiv  14248  fsumconst  15736  fprodconst  15922  isprm5  16644  acsfn2  17607  ghmeql  19115  subgdmdprd  19904  lssvsubcl  20554  lssvacl  20565  ocvin  21227  lindfmm  21382  sraassab  21422  scmatghm  22035  scmatmhm  22036  slesolinv  22182  slesolinvbi  22183  slesolex  22184  pm2mpf1lem  22296  pm2mpcoe1  22302  reftr  23018  alexsubALTlem2  23552  alexsubALTlem3  23553  blbas  23936  nmoco  24254  cncfmet  24425  cmetcaulem  24805  mbflimsup  25183  ulmdvlem3  25914  ptolemy  26006  sltsolem1  27178  madebdaylemlrcut  27393  3wlkdlem6  29418  vdn0conngrumgrv2  29449  frgrncvvdeqlem8  29559  frgrwopreglem5ALT  29575  grpoideu  29762  ipblnfi  30108  htthlem  30170  hvaddsub4  30331  bralnfn  31201  hmops  31273  hmopm  31274  adjadd  31346  opsqrlem1  31393  atomli  31635  chirredlem2  31644  atcvat3i  31649  mdsymlem5  31660  cdj1i  31686  derangenlem  34162  elmrsubrn  34511  dfon2lem6  34760  pibt2  36298  matunitlindflem1  36484  mblfinlem1  36525  prdsbnd  36661  heibor1lem  36677  hl2at  38276  congneg  41708  jm2.26  41741  stoweidlem34  44750  fmtnofac2lem  46236  lindslinindsimp2  47144  ltsubaddb  47195  ltsubadd2b  47197  aacllem  47848