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  5767  fcof1o  5833  infnfi  6953  addcomnqg  7443  addassnqg  7444  nqtri3or  7458  ltexnqq  7470  nqnq0pi  7500  nqpnq0nq  7515  nqnq0a  7516  addassnq0lemcl  7523  ltaddpr  7659  ltexprlemloc  7669  addcanprlemu  7677  recexprlem1ssu  7696  aptiprleml  7701  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  aptisr  7841  mulcnsr  7897  cnegex  8199  muladd  8405  lemul12b  8882  qaddcl  9703  iooshf  10021  elfzomelpfzo  10301  expnegzap  10647  setscom  12661  grplmulf1o  13149  lmodfopne  13825  cnpnei  14398  cxplt3  15095  cxple3  15096