Theorem ad2ant2lr 493

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpteqb  5282  fiunsnnn  6365  addcomnqg  6571  addassnqg  6572  nqtri3or  6586  lt2addnq  6594  lt2mulnq  6595  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  nqpnq0nq  6643  nqnq0a  6644  distrnq0  6649  addassnq0lemcl  6651  ltsrprg  6924  mulcomsrg  6934  mulasssrg  6935  distrsrg  6936  aptisr  6955  mulcnsr  7003  cnegex  7286  sub4  7353  muladd  7488  ltleadd  7550  divdivdivap  7801  divadddivap  7815  ltmul12a  7938  fzrev  9101  facndiv  9666  cncongr1  10485