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  6948  poseq  8088  omxpenlem  8991  fineqvlem  9150  marypha1lem  9317  fin23lem26  10216  axdc3lem4  10344  mulcmpblnr  10962  ltsrpr  10968  sub4  11406  muladd  11549  ltleadd  11600  divdivdiv  11822  divadddiv  11836  ltmul12a  11977  lt2mul2div  12000  xlemul1a  13187  fzrev  13487  facndiv  14195  fsumconst  15697  fprodconst  15885  isprm5  16618  acsfn2  17569  ghmeql  19152  subgdmdprd  19949  lssvacl  20877  lssvsubcl  20878  ocvin  21612  lindfmm  21765  sraassab  21806  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  30143  vdn0conngrumgrv2  30174  frgrncvvdeqlem8  30284  frgrwopreglem5ALT  30300  grpoideu  30487  ipblnfi  30833  htthlem  30895  hvaddsub4  31056  bralnfn  31926  hmops  31998  hmopm  31999  adjadd  32071  opsqrlem1  32118  atomli  32360  chirredlem2  32369  atcvat3i  32374  mdsymlem5  32385  cdj1i  32411  derangenlem  35213  elmrsubrn  35562  dfon2lem6  35828  pibt2  37457  matunitlindflem1  37662  mblfinlem1  37703  prdsbnd  37839  heibor1lem  37855  hl2at  39450  congneg  43008  jm2.26  43041  stoweidlem34  46078  fmtnofac2lem  47605  lindslinindsimp2  48501  ltsubaddb  48552  ltsubadd2b  48554  aacllem  49839