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  5725  fcof1o  5790  infnfi  6895  addcomnqg  7380  addassnqg  7381  nqtri3or  7395  ltexnqq  7407  nqnq0pi  7437  nqpnq0nq  7452  nqnq0a  7453  addassnq0lemcl  7460  ltaddpr  7596  ltexprlemloc  7606  addcanprlemu  7614  recexprlem1ssu  7633  aptiprleml  7638  mulcomsrg  7756  mulasssrg  7757  distrsrg  7758  aptisr  7778  mulcnsr  7834  cnegex  8135  muladd  8341  lemul12b  8818  qaddcl  9635  iooshf  9952  elfzomelpfzo  10231  expnegzap  10554  setscom  12502  grplmulf1o  12944  lmodfopne  13416  cnpnei  13722  cxplt3  14343  cxple3  14344