Theorem ad2ant2rl 480

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  fvtp1g  5369  fcof1o  5429  addcomnqg  6479  addassnqg  6480  nqtri3or  6494  ltexnqq  6506  nqnq0pi  6536  nqpnq0nq  6551  nqnq0a  6552  addassnq0lemcl  6559  ltaddpr  6695  ltexprlemloc  6705  addcanprlemu  6713  recexprlem1ssu  6732  aptiprleml  6737  mulcomsrg  6842  mulasssrg  6843  distrsrg  6844  aptisr  6863  mulcnsr  6911  cnegex  7189  muladd  7381  lemul12b  7827  qaddcl  8570  iooshf  8821  elfzomelpfzo  9087  expnegzap  9289