Theorem ad2ant2lr 761

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 730	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 727	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpteqb  7013  poseq  8177  omxpenlem  9100  fineqvlem  9260  marypha1lem  9428  fin23lem26  10406  axdc3lem4  10534  mulcmpblnr  11159  ltsrpr  11165  sub4  11606  muladd  11751  ltleadd  11802  divdivdiv  12021  divadddiv  12035  ltmul12a  12176  lt2mul2div  12198  xlemul1a  13421  fzrev  13724  facndiv  14435  fsumconst  15961  fprodconst  16150  isprm5  16888  acsfn2  17842  ghmeql  19458  subgdmdprd  20255  lssvacl  21223  lssvsubcl  21224  ocvin  21985  lindfmm  22138  sraassab  22181  scmatghm  22853  scmatmhm  22854  matunitlindflem1  22999  slesolinv  23003  slesolinvbi  23004  slesolex  23005  pm2mpf1lem  23117  pm2mpcoe1  23123  reftr  23838  alexsubALTlem2  24372  alexsubALTlem3  24373  blbas  24754  nmoco  25061  cncfmet  25235  cmetcaulem  25614  mbflimsup  25992  ulmdvlem3  26734  ptolemy  26830  ltssolem1  28037  madebdaylemlrcut  28290  3wlkdlem6  30771  vdn0conngrumgrv2  30802  frgrncvvdeqlem8  30912  frgrwopreglem5ALT  30928  grpoideu  31116  ipblnfi  31462  htthlem  31524  hvaddsub4  31685  bralnfn  32555  hmops  32627  hmopm  32628  adjadd  32700  opsqrlem1  32747  atomli  32989  chirredlem2  32998  atcvat3i  33003  mdsymlem5  33014  cdj1i  33040  derangenlem  36022  elmrsubrn  36371  dfon2lem6  36642  pibt2  38433  mblfinlem1  38668  prdsbnd  38820  heibor1lem  38836  hl2at  40555  congneg  44069  jm2.26  44102  stoweidlem34  47137  fmtnofac2lem  48746  lindslinindsimp2  49668  ltsubaddb  49719  ltsubadd2b  49721  aacllem  51107