Theorem ad2ant2lr 497

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 466	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 463	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  mpteqb  5443  fiunsnnn  6704  addcomnqg  7090  addassnqg  7091  nqtri3or  7105  lt2addnq  7113  lt2mulnq  7114  enq0ref  7142  enq0tr  7143  nqnq0pi  7147  nqpnq0nq  7162  nqnq0a  7163  distrnq0  7168  addassnq0lemcl  7170  ltsrprg  7443  mulcomsrg  7453  mulasssrg  7454  distrsrg  7455  aptisr  7474  mulcnsr  7522  cnegex  7811  sub4  7878  muladd  8013  ltleadd  8075  divdivdivap  8334  divadddivap  8348  ltmul12a  8476  fzrev  9705  facndiv  10326  cncongr1  11577  blbas  12361  cncfmet  12492