Theorem ad2ant2rl 762

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  xpsntpg  7138  poseq  8157  omwordri  8562  omxpenlem  9079  infxpabs  10216  domfin4  10316  isf32lem7  10364  ordpipq  10954  muladd  11673  lemul12b  12099  mulge0b  12112  qaddcl  13018  iooshf  13482  elfzomelpfzo  13831  expnegz  14163  swrdccatin1  14797  bitsshft  16568  setscom  17275  lubun  18606  grplmulf1o  19139  grpraddf1o  19140  srhmsubc  20845  lmodfopne  21087  lidl1el  21417  frlmipval  21995  en2top  23213  cnpnei  23492  kgenidm  23776  ufileu  24148  fmfnfmlem4  24186  isngp4  24841  fsumcn  25101  evth  25190  cmslssbn  25603  mbfmulc2lem  25878  itg1addlem4  25930  dgreq0  26494  cxplt3  26940  cxple3  26941  basellem4  27323  ltssolem1  27914  nodenselem7  27929  zmulscld  28665  axcontlem2  29425  umgr2edg  29672  nbumgrvtx  29809  clwwlkf1  30522  umgrhashecclwwlk  30551  frgrncvvdeqlem9  30790  frgrwopreglem5ALT  30805  numclwwlk7lem  30872  grpoidinvlem3  30990  grpoideu  30993  grporcan  31002  3oalem2  32147  hmops  32504  adjadd  32577  mdslmd4i  32817  mdexchi  32819  mdsymlem1  32887  bnj607  35428  cvxsconn  35825  tailfb  36999  lindsadd  38370  poimirlem14  38386  mblfinlem4  38412  ismblfin  38413  ismtyres  38561  ghomco  38644  rngoisocnv  38734  1idl  38779  ps-2  40354  cfsetsnfsetf1  47950  usgrgrtrirex  48869  grlictr  48934  gpgvtx0  48972  srhmsubcALTV  49243  aacllem  50775