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  8098  omwordri  8497  omxpenlem  9004  infxpabs  10119  domfin4  10219  isf32lem7  10267  ordpipq  10851  muladd  11567  lemul12b  11996  mulge0b  12010  qaddcl  12876  iooshf  13340  elfzomelpfzo  13686  expnegz  14017  swrdccatin1  14646  bitsshft  16400  setscom  17105  lubun  18436  grplmulf1o  18941  grpraddf1o  18942  srhmsubc  20611  lmodfopne  20849  lidl1el  21179  frlmipval  21732  en2top  22927  cnpnei  23206  kgenidm  23489  ufileu  23861  fmfnfmlem4  23899  isngp4  24554  fsumcn  24815  evth  24912  cmslssbn  25326  mbfmulc2lem  25602  itg1addlem4  25654  dgreq0  26225  cxplt3  26663  cxple3  26664  basellem4  27048  sltsolem1  27641  nodenselem7  27656  zmulscld  28355  axcontlem2  28987  umgr2edg  29231  nbumgrvtx  29368  clwwlkf1  30073  umgrhashecclwwlk  30102  frgrncvvdeqlem9  30331  frgrwopreglem5ALT  30346  numclwwlk7lem  30413  grpoidinvlem3  30530  grpoideu  30533  grporcan  30542  3oalem2  31687  hmops  32044  adjadd  32117  mdslmd4i  32357  mdexchi  32359  mdsymlem1  32427  bnj607  35021  cvxsconn  35386  tailfb  36520  lindsadd  37753  poimirlem14  37774  mblfinlem4  37800  ismblfin  37801  ismtyres  37948  ghomco  38031  rngoisocnv  38121  1idl  38166  ps-2  39677  cfsetsnfsetf1  47247  usgrgrtrirex  48138  grlictr  48203  gpgvtx0  48241  srhmsubcALTV  48513  aacllem  49988