Theorem ad2ant2rl 781

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2rl	⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2rl

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 748	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 747	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  omwordri  7539  omxpenlem  7946  infxpabs  8917  domfin4  9016  isf32lem7  9064  ordpipq  9643  muladd  10341  lemul12b  10759  mulge0b  10772  qaddcl  11680  iooshf  12123  elfzomelpfzo  12438  expnegz  12756  bitsshft  15035  setscom  15731  catideu  16159  lubun  16946  grplmulf1o  17312  lmodfopne  18724  lidl1el  19039  frlmipval  19937  en2top  20600  cnpnei  20878  kgenidm  21160  ufileu  21533  fmfnfmlem4  21571  isngp4  22226  fsumcn  22481  evth  22566  mbfmulc2lem  23220  itg1addlem4  23272  dgreq0  23825  cxplt3  24246  cxple3  24247  basellem4  24610  axcontlem2  25645  usgra2adedgspth  26141  usghashecclwwlk  26362  grpoidinvlem3  26744  grpoideu  26747  grporcan  26756  3oalem2  27906  hmops  28263  adjadd  28336  mdslmd4i  28576  mdexchi  28578  mdsymlem1  28646  bnj607  30240  cvxscon  30479  poseq  30994  sltsolem1  31067  nodenselem5  31084  tailfb  31542  poimirlem14  32593  mblfinlem4  32619  ismblfin  32620  ismtyres  32777  ghomco  32860  rngoisocnv  32950  1idl  32995  ps-2  33782  umgr2edg  40436  nbumgrvtx  40568  umgrhashecclwwlk  41262  av-numclwwlk7lem  41543  srhmsubc  41868  srhmsubcALTV  41887  aacllem  42356