Theorem ad2ant2rl 746

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 713	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 712	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:  omwordri  8403  omxpenlem  8860  infxpabs  9968  domfin4  10067  isf32lem7  10115  ordpipq  10698  muladd  11407  lemul12b  11832  mulge0b  11845  qaddcl  12705  iooshf  13158  elfzomelpfzo  13491  expnegz  13817  swrdccatin1  14438  bitsshft  16182  setscom  16881  lubun  18233  grplmulf1o  18649  lmodfopne  20161  lidl1el  20489  frlmipval  20986  en2top  22135  cnpnei  22415  kgenidm  22698  ufileu  23070  fmfnfmlem4  23108  isngp4  23768  fsumcn  24033  evth  24122  cmslssbn  24536  mbfmulc2lem  24811  itg1addlem4  24863  itg1addlem4OLD  24864  dgreq0  25426  cxplt3  25855  cxple3  25856  basellem4  26233  axcontlem2  27333  umgr2edg  27576  nbumgrvtx  27713  clwwlkf1  28413  umgrhashecclwwlk  28442  frgrncvvdeqlem9  28671  frgrwopreglem5ALT  28686  numclwwlk7lem  28753  grpoidinvlem3  28868  grpoideu  28871  grporcan  28880  3oalem2  30025  hmops  30382  adjadd  30455  mdslmd4i  30695  mdexchi  30697  mdsymlem1  30765  bnj607  32896  cvxsconn  33205  poseq  33802  sltsolem1  33878  nodenselem7  33893  tailfb  34566  lindsadd  35770  poimirlem14  35791  mblfinlem4  35817  ismblfin  35818  ismtyres  35966  ghomco  36049  rngoisocnv  36139  1idl  36184  ps-2  37492  cfsetsnfsetf1  44553  srhmsubc  45634  srhmsubcALTV  45652  aacllem  46505