Theorem ad2ant2rl 761

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

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  poseq  8150  omwordri  8553  omxpenlem  9062  infxpabs  10190  domfin4  10290  isf32lem7  10338  ordpipq  10922  muladd  11641  lemul12b  12067  mulge0b  12080  qaddcl  12984  iooshf  13448  elfzomelpfzo  13797  expnegz  14128  swrdccatin1  14758  bitsshft  16528  setscom  17235  lubun  18566  grplmulf1o  19074  grpraddf1o  19075  srhmsubc  20779  lmodfopne  21021  lidl1el  21351  frlmipval  21929  en2top  23142  cnpnei  23421  kgenidm  23704  ufileu  24076  fmfnfmlem4  24114  isngp4  24769  fsumcn  25029  evth  25118  cmslssbn  25531  mbfmulc2lem  25806  itg1addlem4  25858  dgreq0  26422  cxplt3  26865  cxple3  26866  basellem4  27248  ltssolem1  27839  nodenselem7  27854  zmulscld  28590  axcontlem2  29315  umgr2edg  29559  nbumgrvtx  29696  clwwlkf1  30400  umgrhashecclwwlk  30429  frgrncvvdeqlem9  30658  frgrwopreglem5ALT  30673  numclwwlk7lem  30740  grpoidinvlem3  30858  grpoideu  30861  grporcan  30870  3oalem2  32015  hmops  32372  adjadd  32445  mdslmd4i  32685  mdexchi  32687  mdsymlem1  32755  bnj607  35304  cvxsconn  35735  tailfb  36908  lindsadd  38284  poimirlem14  38305  mblfinlem4  38331  ismblfin  38332  ismtyres  38479  ghomco  38562  rngoisocnv  38652  1idl  38697  ps-2  40272  cfsetsnfsetf1  47816  usgrgrtrirex  48735  grlictr  48800  gpgvtx0  48838  srhmsubcALTV  49110  aacllem  50641