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  5792  fcof1o  5858  infnfi  6992  addcomnqg  7494  addassnqg  7495  nqtri3or  7509  ltexnqq  7521  nqnq0pi  7551  nqpnq0nq  7566  nqnq0a  7567  addassnq0lemcl  7574  ltaddpr  7710  ltexprlemloc  7720  addcanprlemu  7728  recexprlem1ssu  7747  aptiprleml  7752  mulcomsrg  7870  mulasssrg  7871  distrsrg  7872  aptisr  7892  mulcnsr  7948  cnegex  8250  muladd  8456  lemul12b  8934  qaddcl  9756  iooshf  10074  elfzomelpfzo  10360  expnegzap  10718  setscom  12872  grplmulf1o  13406  lmodfopne  14088  cnpnei  14691  cxplt3  15392  cxple3  15393