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  5773  fcof1o  5839  infnfi  6965  addcomnqg  7467  addassnqg  7468  nqtri3or  7482  ltexnqq  7494  nqnq0pi  7524  nqpnq0nq  7539  nqnq0a  7540  addassnq0lemcl  7547  ltaddpr  7683  ltexprlemloc  7693  addcanprlemu  7701  recexprlem1ssu  7720  aptiprleml  7725  mulcomsrg  7843  mulasssrg  7844  distrsrg  7845  aptisr  7865  mulcnsr  7921  cnegex  8223  muladd  8429  lemul12b  8907  qaddcl  9728  iooshf  10046  elfzomelpfzo  10326  expnegzap  10684  setscom  12745  grplmulf1o  13278  lmodfopne  13960  cnpnei  14563  cxplt3  15264  cxple3  15265