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  7155  poseq  8188  omwordri  8594  omxpenlem  9111  infxpabs  10302  domfin4  10402  isf32lem7  10450  ordpipq  11040  muladd  11761  lemul12b  12187  mulge0b  12200  qaddcl  13106  iooshf  13570  elfzomelpfzo  13920  expnegz  14252  swrdccatin1  14888  bitsshft  16660  setscom  17373  lubun  18704  grplmulf1o  19238  grpraddf1o  19239  srhmsubc  20947  lmodfopne  21190  lidl1el  21520  frlmipval  22100  en2top  23318  cnpnei  23597  kgenidm  23881  ufileu  24253  fmfnfmlem4  24291  isngp4  24946  fsumcn  25206  evth  25295  cmslssbn  25708  mbfmulc2lem  25983  itg1addlem4  26035  dgreq0  26599  cxplt3  27043  cxple3  27044  basellem4  27426  ltssolem1  28047  nodenselem7  28062  zmulscld  28798  axcontlem2  29558  umgr2edg  29805  nbumgrvtx  29942  clwwlkf1  30655  umgrhashecclwwlk  30684  frgrncvvdeqlem9  30923  frgrwopreglem5ALT  30938  numclwwlk7lem  31005  grpoidinvlem3  31123  grpoideu  31126  grporcan  31135  3oalem2  32280  hmops  32637  adjadd  32710  mdslmd4i  32950  mdexchi  32952  mdsymlem1  33020  bnj607  35602  cvxsconn  36132  tailfb  37295  lindsadd  38679  poimirlem14  38695  mblfinlem4  38721  ismblfin  38722  ismtyres  38885  ghomco  38968  rngoisocnv  39058  1idl  39103  ps-2  40678  cfsetsnfsetf1  48271  usgrgrtrirex  49190  grlictr  49255  gpgvtx0  49293  srhmsubcALTV  49564  aacllem  51156