Theorem ad2ant2rl 747

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 714	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 713	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  omwordri  8192  omxpenlem  8612  infxpabs  9628  domfin4  9727  isf32lem7  9775  ordpipq  10358  muladd  11066  lemul12b  11491  mulge0b  11504  qaddcl  12358  iooshf  12809  elfzomelpfzo  13135  expnegz  13457  swrdccatin1  14081  bitsshft  15818  setscom  16521  lubun  17727  grplmulf1o  18167  lmodfopne  19666  lidl1el  19985  frlmipval  20917  en2top  21587  cnpnei  21866  kgenidm  22149  ufileu  22521  fmfnfmlem4  22559  isngp4  23215  fsumcn  23472  evth  23557  cmslssbn  23969  mbfmulc2lem  24242  itg1addlem4  24294  dgreq0  24849  cxplt3  25277  cxple3  25278  basellem4  25655  axcontlem2  26745  umgr2edg  26985  nbumgrvtx  27122  clwwlkf1  27822  umgrhashecclwwlk  27851  frgrncvvdeqlem9  28080  frgrwopreglem5ALT  28095  numclwwlk7lem  28162  grpoidinvlem3  28277  grpoideu  28280  grporcan  28289  3oalem2  29434  hmops  29791  adjadd  29864  mdslmd4i  30104  mdexchi  30106  mdsymlem1  30174  bnj607  32183  cvxsconn  32485  poseq  33090  sltsolem1  33175  nodenselem7  33189  tailfb  33720  lindsadd  34879  poimirlem14  34900  mblfinlem4  34926  ismblfin  34927  ismtyres  35080  ghomco  35163  rngoisocnv  35253  1idl  35298  ps-2  36608  srhmsubc  44340  srhmsubcALTV  44358  aacllem  44895