Theorem ad2ant2rl 496

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  fvtp1g  5544  fcof1o  5606  infnfi  6691  addcomnqg  7037  addassnqg  7038  nqtri3or  7052  ltexnqq  7064  nqnq0pi  7094  nqpnq0nq  7109  nqnq0a  7110  addassnq0lemcl  7117  ltaddpr  7253  ltexprlemloc  7263  addcanprlemu  7271  recexprlem1ssu  7290  aptiprleml  7295  mulcomsrg  7400  mulasssrg  7401  distrsrg  7402  aptisr  7421  mulcnsr  7469  cnegex  7757  muladd  7959  lemul12b  8419  qaddcl  9219  iooshf  9518  elfzomelpfzo  9791  expnegzap  10104  setscom  11683  cnpnei  12070