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  5606  fiunsnnn  6880  addcomnqg  7379  addassnqg  7380  nqtri3or  7394  lt2addnq  7402  lt2mulnq  7403  enq0ref  7431  enq0tr  7432  nqnq0pi  7436  nqpnq0nq  7451  nqnq0a  7452  distrnq0  7457  addassnq0lemcl  7459  ltsrprg  7745  mulcomsrg  7755  mulasssrg  7756  distrsrg  7757  aptisr  7777  mulcnsr  7833  cnegex  8134  sub4  8201  muladd  8340  ltleadd  8402  divdivdivap  8669  divadddivap  8683  ltmul12a  8816  fzrev  10083  facndiv  10718  cncongr1  12102  blbas  13903  cncfmet  14049  ptolemy  14215