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  5815  fcof1o  5881  infnfi  7018  addcomnqg  7529  addassnqg  7530  nqtri3or  7544  ltexnqq  7556  nqnq0pi  7586  nqpnq0nq  7601  nqnq0a  7602  addassnq0lemcl  7609  ltaddpr  7745  ltexprlemloc  7755  addcanprlemu  7763  recexprlem1ssu  7782  aptiprleml  7787  mulcomsrg  7905  mulasssrg  7906  distrsrg  7907  aptisr  7927  mulcnsr  7983  cnegex  8285  muladd  8491  lemul12b  8969  qaddcl  9791  iooshf  10109  elfzomelpfzo  10397  expnegzap  10755  swrdccatin1  11216  setscom  12987  grplmulf1o  13521  lmodfopne  14203  cnpnei  14806  cxplt3  15507  cxple3  15508