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  5727  fiunsnnn  7051  addcomnqg  7579  addassnqg  7580  nqtri3or  7594  lt2addnq  7602  lt2mulnq  7603  enq0ref  7631  enq0tr  7632  nqnq0pi  7636  nqpnq0nq  7651  nqnq0a  7652  distrnq0  7657  addassnq0lemcl  7659  ltsrprg  7945  mulcomsrg  7955  mulasssrg  7956  distrsrg  7957  aptisr  7977  mulcnsr  8033  cnegex  8335  sub4  8402  muladd  8541  ltleadd  8604  divdivdivap  8871  divadddivap  8885  ltmul12a  9018  fzrev  10292  facndiv  10973  cncongr1  12640  ghmeql  13819  blbas  15122  cncfmet  15281  ptolemy  15513