Theorem ad2ant2rl 748

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  poseq  8144  omwordri  8572  omxpenlem  9073  infxpabs  10207  domfin4  10306  isf32lem7  10354  ordpipq  10937  muladd  11646  lemul12b  12071  mulge0b  12084  qaddcl  12949  iooshf  13403  elfzomelpfzo  13736  expnegz  14062  swrdccatin1  14675  bitsshft  16416  setscom  17113  lubun  18468  grplmulf1o  18897  lmodfopne  20510  lidl1el  20841  frlmipval  21334  en2top  22488  cnpnei  22768  kgenidm  23051  ufileu  23423  fmfnfmlem4  23461  isngp4  24121  fsumcn  24386  evth  24475  cmslssbn  24889  mbfmulc2lem  25164  itg1addlem4  25216  itg1addlem4OLD  25217  dgreq0  25779  cxplt3  26208  cxple3  26209  basellem4  26588  sltsolem1  27178  nodenselem7  27193  axcontlem2  28223  umgr2edg  28466  nbumgrvtx  28603  clwwlkf1  29302  umgrhashecclwwlk  29331  frgrncvvdeqlem9  29560  frgrwopreglem5ALT  29575  numclwwlk7lem  29642  grpoidinvlem3  29759  grpoideu  29762  grporcan  29771  3oalem2  30916  hmops  31273  adjadd  31346  mdslmd4i  31586  mdexchi  31588  mdsymlem1  31656  bnj607  33927  cvxsconn  34234  tailfb  35262  lindsadd  36481  poimirlem14  36502  mblfinlem4  36528  ismblfin  36529  ismtyres  36676  ghomco  36759  rngoisocnv  36849  1idl  36894  ps-2  38349  cfsetsnfsetf1  45769  srhmsubc  46974  srhmsubcALTV  46992  aacllem  47848