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 396

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 206  df-an 397

This theorem is referenced by:  poseq  8146  omwordri  8574  omxpenlem  9075  infxpabs  10209  domfin4  10308  isf32lem7  10356  ordpipq  10939  muladd  11648  lemul12b  12073  mulge0b  12086  qaddcl  12951  iooshf  13405  elfzomelpfzo  13738  expnegz  14064  swrdccatin1  14677  bitsshft  16418  setscom  17115  lubun  18470  grplmulf1o  18899  lmodfopne  20515  lidl1el  20847  frlmipval  21340  en2top  22495  cnpnei  22775  kgenidm  23058  ufileu  23430  fmfnfmlem4  23468  isngp4  24128  fsumcn  24393  evth  24482  cmslssbn  24896  mbfmulc2lem  25171  itg1addlem4  25223  itg1addlem4OLD  25224  dgreq0  25786  cxplt3  26215  cxple3  26216  basellem4  26595  sltsolem1  27185  nodenselem7  27200  axcontlem2  28261  umgr2edg  28504  nbumgrvtx  28641  clwwlkf1  29340  umgrhashecclwwlk  29369  frgrncvvdeqlem9  29598  frgrwopreglem5ALT  29613  numclwwlk7lem  29680  grpoidinvlem3  29797  grpoideu  29800  grporcan  29809  3oalem2  30954  hmops  31311  adjadd  31384  mdslmd4i  31624  mdexchi  31626  mdsymlem1  31694  bnj607  33996  cvxsconn  34303  tailfb  35348  lindsadd  36567  poimirlem14  36588  mblfinlem4  36614  ismblfin  36615  ismtyres  36762  ghomco  36845  rngoisocnv  36935  1idl  36980  ps-2  38435  cfsetsnfsetf1  45848  srhmsubc  47053  srhmsubcALTV  47071  aacllem  47926