Theorem ad2ant2rl 750

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 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 716	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  8110  omwordri  8509  omxpenlem  9018  infxpabs  10133  domfin4  10233  isf32lem7  10281  ordpipq  10865  muladd  11581  lemul12b  12010  mulge0b  12024  qaddcl  12890  iooshf  13354  elfzomelpfzo  13700  expnegz  14031  swrdccatin1  14660  bitsshft  16414  setscom  17119  lubun  18450  grplmulf1o  18958  grpraddf1o  18959  srhmsubc  20628  lmodfopne  20866  lidl1el  21196  frlmipval  21749  en2top  22944  cnpnei  23223  kgenidm  23506  ufileu  23878  fmfnfmlem4  23916  isngp4  24571  fsumcn  24832  evth  24929  cmslssbn  25343  mbfmulc2lem  25619  itg1addlem4  25671  dgreq0  26242  cxplt3  26680  cxple3  26681  basellem4  27065  ltssolem1  27658  nodenselem7  27673  zmulscld  28408  axcontlem2  29054  umgr2edg  29298  nbumgrvtx  29435  clwwlkf1  30140  umgrhashecclwwlk  30169  frgrncvvdeqlem9  30398  frgrwopreglem5ALT  30413  numclwwlk7lem  30480  grpoidinvlem3  30598  grpoideu  30601  grporcan  30610  3oalem2  31755  hmops  32112  adjadd  32185  mdslmd4i  32425  mdexchi  32427  mdsymlem1  32495  bnj607  35096  cvxsconn  35463  tailfb  36597  lindsadd  37868  poimirlem14  37889  mblfinlem4  37915  ismblfin  37916  ismtyres  38063  ghomco  38146  rngoisocnv  38236  1idl  38281  ps-2  39858  cfsetsnfsetf1  47423  usgrgrtrirex  48314  grlictr  48379  gpgvtx0  48417  srhmsubcALTV  48689  aacllem  50164