Theorem ad2ant2rl 515

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 482	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 481	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fvtp1g  5926  fcof1o  5998  infnfi  7205  addcomnqg  7754  addassnqg  7755  nqtri3or  7769  ltexnqq  7781  nqnq0pi  7811  nqpnq0nq  7826  nqnq0a  7827  addassnq0lemcl  7834  ltaddpr  7970  ltexprlemloc  7980  addcanprlemu  7988  recexprlem1ssu  8007  aptiprleml  8012  mulcomsrg  8130  mulasssrg  8131  distrsrg  8132  aptisr  8152  mulcnsr  8208  cnegex  8511  muladd  8718  lemul12b  9199  qaddcl  10050  iooshf  10370  elfzomelpfzo  10665  expnegzap  11030  swrdccatin1  11518  setscom  13449  grplmulf1o  13937  lmodfopne  14771  cnpnei  15462  cxplt3  16172  cxple3  16173  umgr2edg  16670