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  7140  poseq  8159  omwordri  8562  omxpenlem  9079  infxpabs  10216  domfin4  10316  isf32lem7  10364  ordpipq  10954  muladd  11673  lemul12b  12099  mulge0b  12112  qaddcl  13017  iooshf  13481  elfzomelpfzo  13830  expnegz  14162  swrdccatin1  14796  bitsshft  16569  setscom  17276  lubun  18607  grplmulf1o  19140  grpraddf1o  19141  srhmsubc  20846  lmodfopne  21088  lidl1el  21418  frlmipval  21996  en2top  23214  cnpnei  23493  kgenidm  23777  ufileu  24149  fmfnfmlem4  24187  isngp4  24842  fsumcn  25102  evth  25191  cmslssbn  25604  mbfmulc2lem  25879  itg1addlem4  25931  dgreq0  26495  cxplt3  26938  cxple3  26939  basellem4  27321  ltssolem1  27912  nodenselem7  27927  zmulscld  28663  axcontlem2  29423  umgr2edg  29670  nbumgrvtx  29807  clwwlkf1  30520  umgrhashecclwwlk  30549  frgrncvvdeqlem9  30788  frgrwopreglem5ALT  30803  numclwwlk7lem  30870  grpoidinvlem3  30988  grpoideu  30991  grporcan  31000  3oalem2  32145  hmops  32502  adjadd  32575  mdslmd4i  32815  mdexchi  32817  mdsymlem1  32885  bnj607  35427  cvxsconn  35824  tailfb  36998  lindsadd  38369  poimirlem14  38385  mblfinlem4  38411  ismblfin  38412  ismtyres  38560  ghomco  38643  rngoisocnv  38733  1idl  38778  ps-2  40353  cfsetsnfsetf1  47949  usgrgrtrirex  48868  grlictr  48933  gpgvtx0  48971  srhmsubcALTV  49242  aacllem  50774