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  6894  omxpenlem  8860  fineqvlem  9037  marypha1lem  9192  fin23lem26  10081  axdc3lem4  10209  mulcmpblnr  10827  ltsrpr  10833  sub4  11266  muladd  11407  ltleadd  11458  divdivdiv  11676  divadddiv  11690  ltmul12a  11831  lt2mul2div  11853  xlemul1a  13022  fzrev  13319  facndiv  14002  fsumconst  15502  fprodconst  15688  isprm5  16412  acsfn2  17372  ghmeql  18857  subgdmdprd  19637  lssvsubcl  20205  lssvacl  20216  ocvin  20879  lindfmm  21034  scmatghm  21682  scmatmhm  21683  slesolinv  21829  slesolinvbi  21830  slesolex  21831  pm2mpf1lem  21943  pm2mpcoe1  21949  reftr  22665  alexsubALTlem2  23199  alexsubALTlem3  23200  blbas  23583  nmoco  23901  cncfmet  24072  cmetcaulem  24452  mbflimsup  24830  ulmdvlem3  25561  ptolemy  25653  3wlkdlem6  28529  vdn0conngrumgrv2  28560  frgrncvvdeqlem8  28670  frgrwopreglem5ALT  28686  grpoideu  28871  ipblnfi  29217  htthlem  29279  hvaddsub4  29440  bralnfn  30310  hmops  30382  hmopm  30383  adjadd  30455  opsqrlem1  30502  atomli  30744  chirredlem2  30753  atcvat3i  30758  mdsymlem5  30769  cdj1i  30795  derangenlem  33133  elmrsubrn  33482  dfon2lem6  33764  poseq  33802  sltsolem1  33878  madebdaylemlrcut  34079  pibt2  35588  matunitlindflem1  35773  mblfinlem1  35814  prdsbnd  35951  heibor1lem  35967  hl2at  37419  congneg  40791  jm2.26  40824  stoweidlem34  43575  fmtnofac2lem  45020  lindslinindsimp2  45804  ltsubaddb  45855  ltsubadd2b  45857  aacllem  46505