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  5870  fcof1o  5940  infnfi  7127  addcomnqg  7644  addassnqg  7645  nqtri3or  7659  ltexnqq  7671  nqnq0pi  7701  nqpnq0nq  7716  nqnq0a  7717  addassnq0lemcl  7724  ltaddpr  7860  ltexprlemloc  7870  addcanprlemu  7878  recexprlem1ssu  7897  aptiprleml  7902  mulcomsrg  8020  mulasssrg  8021  distrsrg  8022  aptisr  8042  mulcnsr  8098  cnegex  8399  muladd  8605  lemul12b  9083  qaddcl  9913  iooshf  10231  elfzomelpfzo  10522  expnegzap  10881  swrdccatin1  11355  setscom  13185  grplmulf1o  13720  lmodfopne  14405  cnpnei  15013  cxplt3  15714  cxple3  15715  umgr2edg  16131