Theorem ad2ant2rl 502

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  fvtp1g  5628  fcof1o  5690  infnfi  6789  addcomnqg  7189  addassnqg  7190  nqtri3or  7204  ltexnqq  7216  nqnq0pi  7246  nqpnq0nq  7261  nqnq0a  7262  addassnq0lemcl  7269  ltaddpr  7405  ltexprlemloc  7415  addcanprlemu  7423  recexprlem1ssu  7442  aptiprleml  7447  mulcomsrg  7565  mulasssrg  7566  distrsrg  7567  aptisr  7587  mulcnsr  7643  cnegex  7940  muladd  8146  lemul12b  8619  qaddcl  9427  iooshf  9735  elfzomelpfzo  10008  expnegzap  10327  setscom  11999  cnpnei  12388