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  8140  omwordri  8568  omxpenlem  9069  infxpabs  10203  domfin4  10302  isf32lem7  10350  ordpipq  10933  muladd  11642  lemul12b  12067  mulge0b  12080  qaddcl  12945  iooshf  13399  elfzomelpfzo  13732  expnegz  14058  swrdccatin1  14671  bitsshft  16412  setscom  17109  lubun  18464  grplmulf1o  18893  lmodfopne  20502  lidl1el  20833  frlmipval  21325  en2top  22479  cnpnei  22759  kgenidm  23042  ufileu  23414  fmfnfmlem4  23452  isngp4  24112  fsumcn  24377  evth  24466  cmslssbn  24880  mbfmulc2lem  25155  itg1addlem4  25207  itg1addlem4OLD  25208  dgreq0  25770  cxplt3  26199  cxple3  26200  basellem4  26577  sltsolem1  27167  nodenselem7  27182  axcontlem2  28212  umgr2edg  28455  nbumgrvtx  28592  clwwlkf1  29291  umgrhashecclwwlk  29320  frgrncvvdeqlem9  29549  frgrwopreglem5ALT  29564  numclwwlk7lem  29631  grpoidinvlem3  29746  grpoideu  29749  grporcan  29758  3oalem2  30903  hmops  31260  adjadd  31333  mdslmd4i  31573  mdexchi  31575  mdsymlem1  31643  bnj607  33915  cvxsconn  34222  tailfb  35250  lindsadd  36469  poimirlem14  36490  mblfinlem4  36516  ismblfin  36517  ismtyres  36664  ghomco  36747  rngoisocnv  36837  1idl  36882  ps-2  38337  cfsetsnfsetf1  45755  srhmsubc  46927  srhmsubcALTV  46945  aacllem  47801