Theorem ad2ant2lr 749

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 718	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 715	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  6967  poseq  8108  omxpenlem  9016  fineqvlem  9176  marypha1lem  9346  fin23lem26  10247  axdc3lem4  10375  mulcmpblnr  10994  ltsrpr  11000  sub4  11439  muladd  11582  ltleadd  11633  divdivdiv  11856  divadddiv  11870  ltmul12a  12011  lt2mul2div  12034  xlemul1a  13240  fzrev  13541  facndiv  14250  fsumconst  15752  fprodconst  15943  isprm5  16677  acsfn2  17629  ghmeql  19214  subgdmdprd  20011  lssvacl  20938  lssvsubcl  20939  ocvin  21654  lindfmm  21807  sraassab  21848  scmatghm  22498  scmatmhm  22499  slesolinv  22645  slesolinvbi  22646  slesolex  22647  pm2mpf1lem  22759  pm2mpcoe1  22765  reftr  23479  alexsubALTlem2  24013  alexsubALTlem3  24014  blbas  24395  nmoco  24702  cncfmet  24876  cmetcaulem  25255  mbflimsup  25633  ulmdvlem3  26367  ptolemy  26460  ltssolem1  27639  madebdaylemlrcut  27891  3wlkdlem6  30235  vdn0conngrumgrv2  30266  frgrncvvdeqlem8  30376  frgrwopreglem5ALT  30392  grpoideu  30580  ipblnfi  30926  htthlem  30988  hvaddsub4  31149  bralnfn  32019  hmops  32091  hmopm  32092  adjadd  32164  opsqrlem1  32211  atomli  32453  chirredlem2  32462  atcvat3i  32467  mdsymlem5  32478  cdj1i  32504  derangenlem  35353  elmrsubrn  35702  dfon2lem6  35968  pibt2  37733  matunitlindflem1  37937  mblfinlem1  37978  prdsbnd  38114  heibor1lem  38130  hl2at  39851  congneg  43397  jm2.26  43430  stoweidlem34  46462  fmtnofac2lem  48031  lindslinindsimp2  48939  ltsubaddb  48990  ltsubadd2b  48992  aacllem  50276