Theorem ad2ant2rl 759

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  poseq  8138  omwordri  8541  omxpenlem  9050  infxpabs  10167  domfin4  10268  isf32lem7  10316  ordpipq  10900  muladd  11619  lemul12b  12048  mulge0b  12062  qaddcl  12966  iooshf  13430  elfzomelpfzo  13778  expnegz  14109  swrdccatin1  14738  bitsshft  16509  setscom  17216  lubun  18547  grplmulf1o  19055  grpraddf1o  19056  srhmsubc  20730  lmodfopne  20967  lidl1el  21296  frlmipval  21831  en2top  23045  cnpnei  23324  kgenidm  23607  ufileu  23979  fmfnfmlem4  24017  isngp4  24672  fsumcn  24932  evth  25021  cmslssbn  25434  mbfmulc2lem  25709  itg1addlem4  25761  dgreq0  26325  cxplt3  26765  cxple3  26766  basellem4  27148  ltssolem1  27739  nodenselem7  27754  zmulscld  28490  axcontlem2  29166  umgr2edg  29410  nbumgrvtx  29547  clwwlkf1  30251  umgrhashecclwwlk  30280  frgrncvvdeqlem9  30509  frgrwopreglem5ALT  30524  numclwwlk7lem  30591  grpoidinvlem3  30709  grpoideu  30712  grporcan  30721  3oalem2  31866  hmops  32223  adjadd  32296  mdslmd4i  32536  mdexchi  32538  mdsymlem1  32606  bnj607  35211  cvxsconn  35593  tailfb  36737  lindsadd  38112  poimirlem14  38133  mblfinlem4  38159  ismblfin  38160  ismtyres  38307  ghomco  38390  rngoisocnv  38480  1idl  38525  ps-2  40102  cfsetsnfsetf1  47653  usgrgrtrirex  48572  grlictr  48637  gpgvtx0  48675  srhmsubcALTV  48947  aacllem  50422