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  5846  fcof1o  5912  infnfi  7053  addcomnqg  7564  addassnqg  7565  nqtri3or  7579  ltexnqq  7591  nqnq0pi  7621  nqpnq0nq  7636  nqnq0a  7637  addassnq0lemcl  7644  ltaddpr  7780  ltexprlemloc  7790  addcanprlemu  7798  recexprlem1ssu  7817  aptiprleml  7822  mulcomsrg  7940  mulasssrg  7941  distrsrg  7942  aptisr  7962  mulcnsr  8018  cnegex  8320  muladd  8526  lemul12b  9004  qaddcl  9826  iooshf  10144  elfzomelpfzo  10432  expnegzap  10790  swrdccatin1  11252  setscom  13067  grplmulf1o  13602  lmodfopne  14284  cnpnei  14887  cxplt3  15588  cxple3  15589  umgr2edg  15999