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  7144  poseq  8175  omwordri  8580  omxpenlem  9097  infxpabs  10289  domfin4  10389  isf32lem7  10437  ordpipq  11027  muladd  11748  lemul12b  12174  mulge0b  12187  qaddcl  13093  iooshf  13557  elfzomelpfzo  13907  expnegz  14239  swrdccatin1  14874  bitsshft  16645  setscom  17358  lubun  18689  grplmulf1o  19223  grpraddf1o  19224  srhmsubc  20932  lmodfopne  21175  lidl1el  21505  frlmipval  22085  en2top  23303  cnpnei  23582  kgenidm  23866  ufileu  24238  fmfnfmlem4  24276  isngp4  24931  fsumcn  25191  evth  25280  cmslssbn  25693  mbfmulc2lem  25968  itg1addlem4  26020  dgreq0  26584  cxplt3  27028  cxple3  27029  basellem4  27411  ltssolem1  28032  nodenselem7  28047  zmulscld  28783  axcontlem2  29543  umgr2edg  29790  nbumgrvtx  29927  clwwlkf1  30640  umgrhashecclwwlk  30669  frgrncvvdeqlem9  30908  frgrwopreglem5ALT  30923  numclwwlk7lem  30990  grpoidinvlem3  31108  grpoideu  31111  grporcan  31120  3oalem2  32265  hmops  32622  adjadd  32695  mdslmd4i  32935  mdexchi  32937  mdsymlem1  33005  bnj607  35546  cvxsconn  36008  tailfb  37165  lindsadd  38536  poimirlem14  38552  mblfinlem4  38578  ismblfin  38579  ismtyres  38742  ghomco  38825  rngoisocnv  38915  1idl  38960  ps-2  40535  cfsetsnfsetf1  48128  usgrgrtrirex  49047  grlictr  49112  gpgvtx0  49150  srhmsubcALTV  49421  aacllem  50938