Theorem ad2ant2rl 749

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 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 715	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  8183  omwordri  8610  omxpenlem  9113  infxpabs  10251  domfin4  10351  isf32lem7  10399  ordpipq  10982  muladd  11695  lemul12b  12124  mulge0b  12138  qaddcl  13007  iooshf  13466  elfzomelpfzo  13810  expnegz  14137  swrdccatin1  14763  bitsshft  16512  setscom  17217  lubun  18560  grplmulf1o  19031  grpraddf1o  19032  srhmsubc  20680  lmodfopne  20898  lidl1el  21236  frlmipval  21799  en2top  22992  cnpnei  23272  kgenidm  23555  ufileu  23927  fmfnfmlem4  23965  isngp4  24625  fsumcn  24894  evth  24991  cmslssbn  25406  mbfmulc2lem  25682  itg1addlem4  25734  dgreq0  26305  cxplt3  26742  cxple3  26743  basellem4  27127  sltsolem1  27720  nodenselem7  27735  zmulscld  28383  axcontlem2  28980  umgr2edg  29226  nbumgrvtx  29363  clwwlkf1  30068  umgrhashecclwwlk  30097  frgrncvvdeqlem9  30326  frgrwopreglem5ALT  30341  numclwwlk7lem  30408  grpoidinvlem3  30525  grpoideu  30528  grporcan  30537  3oalem2  31682  hmops  32039  adjadd  32112  mdslmd4i  32352  mdexchi  32354  mdsymlem1  32422  bnj607  34930  cvxsconn  35248  tailfb  36378  lindsadd  37620  poimirlem14  37641  mblfinlem4  37667  ismblfin  37668  ismtyres  37815  ghomco  37898  rngoisocnv  37988  1idl  38033  ps-2  39480  cfsetsnfsetf1  47071  usgrgrtrirex  47917  grlictr  47975  gpgvtx0  48008  srhmsubcALTV  48241  aacllem  49320