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  6987  poseq  8137  omxpenlem  9042  fineqvlem  9209  marypha1lem  9384  fin23lem26  10278  axdc3lem4  10406  mulcmpblnr  11024  ltsrpr  11030  sub4  11467  muladd  11610  ltleadd  11661  divdivdiv  11883  divadddiv  11897  ltmul12a  12038  lt2mul2div  12061  xlemul1a  13248  fzrev  13548  facndiv  14253  fsumconst  15756  fprodconst  15944  isprm5  16677  acsfn2  17624  ghmeql  19171  subgdmdprd  19966  lssvacl  20849  lssvsubcl  20850  ocvin  21583  lindfmm  21736  sraassab  21777  scmatghm  22420  scmatmhm  22421  slesolinv  22567  slesolinvbi  22568  slesolex  22569  pm2mpf1lem  22681  pm2mpcoe1  22687  reftr  23401  alexsubALTlem2  23935  alexsubALTlem3  23936  blbas  24318  nmoco  24625  cncfmet  24802  cmetcaulem  25188  mbflimsup  25567  ulmdvlem3  26311  ptolemy  26405  sltsolem1  27587  madebdaylemlrcut  27810  3wlkdlem6  30094  vdn0conngrumgrv2  30125  frgrncvvdeqlem8  30235  frgrwopreglem5ALT  30251  grpoideu  30438  ipblnfi  30784  htthlem  30846  hvaddsub4  31007  bralnfn  31877  hmops  31949  hmopm  31950  adjadd  32022  opsqrlem1  32069  atomli  32311  chirredlem2  32320  atcvat3i  32325  mdsymlem5  32336  cdj1i  32362  derangenlem  35158  elmrsubrn  35507  dfon2lem6  35776  pibt2  37405  matunitlindflem1  37610  mblfinlem1  37651  prdsbnd  37787  heibor1lem  37803  hl2at  39399  congneg  42958  jm2.26  42991  stoweidlem34  46032  fmtnofac2lem  47569  lindslinindsimp2  48452  ltsubaddb  48503  ltsubadd2b  48505  aacllem  49790