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  6954  poseq  8094  omxpenlem  8998  fineqvlem  9157  marypha1lem  9324  fin23lem26  10223  axdc3lem4  10351  mulcmpblnr  10969  ltsrpr  10975  sub4  11413  muladd  11556  ltleadd  11607  divdivdiv  11829  divadddiv  11843  ltmul12a  11984  lt2mul2div  12007  xlemul1a  13189  fzrev  13489  facndiv  14197  fsumconst  15699  fprodconst  15887  isprm5  16620  acsfn2  17571  ghmeql  19153  subgdmdprd  19950  lssvacl  20878  lssvsubcl  20879  ocvin  21613  lindfmm  21766  sraassab  21807  scmatghm  22449  scmatmhm  22450  slesolinv  22596  slesolinvbi  22597  slesolex  22598  pm2mpf1lem  22710  pm2mpcoe1  22716  reftr  23430  alexsubALTlem2  23964  alexsubALTlem3  23965  blbas  24346  nmoco  24653  cncfmet  24830  cmetcaulem  25216  mbflimsup  25595  ulmdvlem3  26339  ptolemy  26433  sltsolem1  27615  madebdaylemlrcut  27845  3wlkdlem6  30147  vdn0conngrumgrv2  30178  frgrncvvdeqlem8  30288  frgrwopreglem5ALT  30304  grpoideu  30491  ipblnfi  30837  htthlem  30899  hvaddsub4  31060  bralnfn  31930  hmops  32002  hmopm  32003  adjadd  32075  opsqrlem1  32122  atomli  32364  chirredlem2  32373  atcvat3i  32378  mdsymlem5  32389  cdj1i  32415  derangenlem  35236  elmrsubrn  35585  dfon2lem6  35851  pibt2  37482  matunitlindflem1  37676  mblfinlem1  37717  prdsbnd  37853  heibor1lem  37869  hl2at  39524  congneg  43086  jm2.26  43119  stoweidlem34  46156  fmtnofac2lem  47692  lindslinindsimp2  48588  ltsubaddb  48639  ltsubadd2b  48641  aacllem  49926