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  5653  fiunsnnn  6943  addcomnqg  7450  addassnqg  7451  nqtri3or  7465  lt2addnq  7473  lt2mulnq  7474  enq0ref  7502  enq0tr  7503  nqnq0pi  7507  nqpnq0nq  7522  nqnq0a  7523  distrnq0  7528  addassnq0lemcl  7530  ltsrprg  7816  mulcomsrg  7826  mulasssrg  7827  distrsrg  7828  aptisr  7848  mulcnsr  7904  cnegex  8206  sub4  8273  muladd  8412  ltleadd  8475  divdivdivap  8742  divadddivap  8756  ltmul12a  8889  fzrev  10161  facndiv  10833  cncongr1  12281  ghmeql  13407  blbas  14679  cncfmet  14838  ptolemy  15070