Theorem ad2ant2lr 510

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2lr	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 479	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 476	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:  mpteqb  5603  fiunsnnn  6876  addcomnqg  7375  addassnqg  7376  nqtri3or  7390  lt2addnq  7398  lt2mulnq  7399  enq0ref  7427  enq0tr  7428  nqnq0pi  7432  nqpnq0nq  7447  nqnq0a  7448  distrnq0  7453  addassnq0lemcl  7455  ltsrprg  7741  mulcomsrg  7751  mulasssrg  7752  distrsrg  7753  aptisr  7773  mulcnsr  7829  cnegex  8129  sub4  8196  muladd  8335  ltleadd  8397  divdivdivap  8664  divadddivap  8678  ltmul12a  8811  fzrev  10077  facndiv  10710  cncongr1  12093  blbas  13715  cncfmet  13861  ptolemy  14027