Theorem ad2ant2rl 511

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  fvtp1g  5857  fcof1o  5925  infnfi  7077  addcomnqg  7591  addassnqg  7592  nqtri3or  7606  ltexnqq  7618  nqnq0pi  7648  nqpnq0nq  7663  nqnq0a  7664  addassnq0lemcl  7671  ltaddpr  7807  ltexprlemloc  7817  addcanprlemu  7825  recexprlem1ssu  7844  aptiprleml  7849  mulcomsrg  7967  mulasssrg  7968  distrsrg  7969  aptisr  7989  mulcnsr  8045  cnegex  8347  muladd  8553  lemul12b  9031  qaddcl  9859  iooshf  10177  elfzomelpfzo  10466  expnegzap  10825  swrdccatin1  11296  setscom  13112  grplmulf1o  13647  lmodfopne  14330  cnpnei  14933  cxplt3  15634  cxple3  15635  umgr2edg  16046