Theorem ad2ant2rl 503

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 470	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantlr 469	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  5636  fcof1o  5698  infnfi  6797  addcomnqg  7213  addassnqg  7214  nqtri3or  7228  ltexnqq  7240  nqnq0pi  7270  nqpnq0nq  7285  nqnq0a  7286  addassnq0lemcl  7293  ltaddpr  7429  ltexprlemloc  7439  addcanprlemu  7447  recexprlem1ssu  7466  aptiprleml  7471  mulcomsrg  7589  mulasssrg  7590  distrsrg  7591  aptisr  7611  mulcnsr  7667  cnegex  7964  muladd  8170  lemul12b  8643  qaddcl  9454  iooshf  9765  elfzomelpfzo  10039  expnegzap  10358  setscom  12038  cnpnei  12427  cxplt3  13048  cxple3  13049