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  7143  poseq  8160  omwordri  8563  omxpenlem  9073  infxpabs  10210  domfin4  10310  isf32lem7  10358  ordpipq  10944  muladd  11663  lemul12b  12089  mulge0b  12102  qaddcl  13007  iooshf  13471  elfzomelpfzo  13820  expnegz  14152  swrdccatin1  14786  bitsshft  16557  setscom  17264  lubun  18595  grplmulf1o  19125  grpraddf1o  19126  srhmsubc  20831  lmodfopne  21073  lidl1el  21403  frlmipval  21981  en2top  23194  cnpnei  23473  kgenidm  23757  ufileu  24129  fmfnfmlem4  24167  isngp4  24822  fsumcn  25082  evth  25171  cmslssbn  25584  mbfmulc2lem  25859  itg1addlem4  25911  dgreq0  26475  cxplt3  26918  cxple3  26919  basellem4  27301  ltssolem1  27892  nodenselem7  27907  zmulscld  28643  axcontlem2  29372  umgr2edg  29619  nbumgrvtx  29756  clwwlkf1  30469  umgrhashecclwwlk  30498  frgrncvvdeqlem9  30731  frgrwopreglem5ALT  30746  numclwwlk7lem  30813  grpoidinvlem3  30931  grpoideu  30934  grporcan  30943  3oalem2  32088  hmops  32445  adjadd  32518  mdslmd4i  32758  mdexchi  32760  mdsymlem1  32828  bnj607  35371  cvxsconn  35774  tailfb  36947  lindsadd  38323  poimirlem14  38344  mblfinlem4  38370  ismblfin  38371  ismtyres  38519  ghomco  38602  rngoisocnv  38692  1idl  38737  ps-2  40312  cfsetsnfsetf1  47856  usgrgrtrirex  48775  grlictr  48840  gpgvtx0  48878  srhmsubcALTV  49149  aacllem  50680