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  5791  fcof1o  5857  infnfi  6991  addcomnqg  7493  addassnqg  7494  nqtri3or  7508  ltexnqq  7520  nqnq0pi  7550  nqpnq0nq  7565  nqnq0a  7566  addassnq0lemcl  7573  ltaddpr  7709  ltexprlemloc  7719  addcanprlemu  7727  recexprlem1ssu  7746  aptiprleml  7751  mulcomsrg  7869  mulasssrg  7870  distrsrg  7871  aptisr  7891  mulcnsr  7947  cnegex  8249  muladd  8455  lemul12b  8933  qaddcl  9755  iooshf  10073  elfzomelpfzo  10358  expnegzap  10716  setscom  12843  grplmulf1o  13377  lmodfopne  14059  cnpnei  14662  cxplt3  15363  cxple3  15364