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  5861  fcof1o  5929  infnfi  7083  addcomnqg  7600  addassnqg  7601  nqtri3or  7615  ltexnqq  7627  nqnq0pi  7657  nqpnq0nq  7672  nqnq0a  7673  addassnq0lemcl  7680  ltaddpr  7816  ltexprlemloc  7826  addcanprlemu  7834  recexprlem1ssu  7853  aptiprleml  7858  mulcomsrg  7976  mulasssrg  7977  distrsrg  7978  aptisr  7998  mulcnsr  8054  cnegex  8356  muladd  8562  lemul12b  9040  qaddcl  9868  iooshf  10186  elfzomelpfzo  10475  expnegzap  10834  swrdccatin1  11305  setscom  13121  grplmulf1o  13656  lmodfopne  14339  cnpnei  14942  cxplt3  15643  cxple3  15644  umgr2edg  16057