Theorem ad2ant2rl 746

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  omwordri  7892  omxpenlem  8303  infxpabs  9322  domfin4  9421  isf32lem7  9469  ordpipq  10052  muladd  10750  lemul12b  11168  mulge0b  11181  qaddcl  12026  iooshf  12473  elfzomelpfzo  12799  expnegz  13120  bitsshft  15419  setscom  16117  lubun  17331  grplmulf1o  17697  lmodfopne  19108  lidl1el  19430  frlmipval  20332  en2top  21007  cnpnei  21286  kgenidm  21568  ufileu  21940  fmfnfmlem4  21978  isngp4  22633  fsumcn  22890  evth  22975  mbfmulc2lem  23634  itg1addlem4  23686  dgreq0  24241  cxplt3  24666  cxple3  24667  basellem4  25030  axcontlem2  26065  umgr2edg  26322  nbumgrvtx  26464  umgrhashecclwwlk  27235  frgrncvvdeqlem9  27488  frgrwopreglem5ALT  27503  numclwwlk7lem  27583  grpoidinvlem3  27695  grpoideu  27698  grporcan  27707  3oalem2  28856  hmops  29213  adjadd  29286  mdslmd4i  29526  mdexchi  29528  mdsymlem1  29596  bnj607  31314  cvxsconn  31553  poseq  32079  sltsolem1  32152  nodenselem7  32166  tailfb  32698  poimirlem14  33738  mblfinlem4  33764  ismblfin  33765  ismtyres  33920  ghomco  34003  rngoisocnv  34093  1idl  34138  ps-2  35260  srhmsubc  42645  srhmsubcALTV  42663  aacllem  43119