Theorem ad2ant2rl 749

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 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 715	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:  poseq  8091  omwordri  8490  omxpenlem  8995  infxpabs  10105  domfin4  10205  isf32lem7  10253  ordpipq  10836  muladd  11552  lemul12b  11981  mulge0b  11995  qaddcl  12866  iooshf  13329  elfzomelpfzo  13674  expnegz  14003  swrdccatin1  14631  bitsshft  16386  setscom  17091  lubun  18421  grplmulf1o  18892  grpraddf1o  18893  srhmsubc  20565  lmodfopne  20803  lidl1el  21133  frlmipval  21686  en2top  22870  cnpnei  23149  kgenidm  23432  ufileu  23804  fmfnfmlem4  23842  isngp4  24498  fsumcn  24759  evth  24856  cmslssbn  25270  mbfmulc2lem  25546  itg1addlem4  25598  dgreq0  26169  cxplt3  26607  cxple3  26608  basellem4  26992  sltsolem1  27585  nodenselem7  27600  zmulscld  28290  axcontlem2  28910  umgr2edg  29154  nbumgrvtx  29291  clwwlkf1  29993  umgrhashecclwwlk  30022  frgrncvvdeqlem9  30251  frgrwopreglem5ALT  30266  numclwwlk7lem  30333  grpoidinvlem3  30450  grpoideu  30453  grporcan  30462  3oalem2  31607  hmops  31964  adjadd  32037  mdslmd4i  32277  mdexchi  32279  mdsymlem1  32347  bnj607  34883  cvxsconn  35220  tailfb  36355  lindsadd  37597  poimirlem14  37618  mblfinlem4  37644  ismblfin  37645  ismtyres  37792  ghomco  37875  rngoisocnv  37965  1idl  38010  ps-2  39461  cfsetsnfsetf1  47047  usgrgrtrirex  47938  grlictr  48003  gpgvtx0  48041  srhmsubcALTV  48313  aacllem  49790