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  5746  fiunsnnn  7113  addcomnqg  7644  addassnqg  7645  nqtri3or  7659  lt2addnq  7667  lt2mulnq  7668  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nqpnq0nq  7716  nqnq0a  7717  distrnq0  7722  addassnq0lemcl  7724  ltsrprg  8010  mulcomsrg  8020  mulasssrg  8021  distrsrg  8022  aptisr  8042  mulcnsr  8098  cnegex  8399  sub4  8466  muladd  8605  ltleadd  8668  divdivdivap  8935  divadddivap  8949  ltmul12a  9082  fzrev  10364  facndiv  11047  cncongr1  12738  ghmeql  13917  blbas  15227  cncfmet  15386  ptolemy  15618