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  5745  fcof1o  5811  infnfi  6924  addcomnqg  7411  addassnqg  7412  nqtri3or  7426  ltexnqq  7438  nqnq0pi  7468  nqpnq0nq  7483  nqnq0a  7484  addassnq0lemcl  7491  ltaddpr  7627  ltexprlemloc  7637  addcanprlemu  7645  recexprlem1ssu  7664  aptiprleml  7669  mulcomsrg  7787  mulasssrg  7788  distrsrg  7789  aptisr  7809  mulcnsr  7865  cnegex  8166  muladd  8372  lemul12b  8849  qaddcl  9667  iooshf  9984  elfzomelpfzo  10263  expnegzap  10588  setscom  12555  grplmulf1o  13033  lmodfopne  13659  cnpnei  14196  cxplt3  14817  cxple3  14818