Theorem ad2ant2lr 507

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpteqb  5584  fiunsnnn  6856  addcomnqg  7332  addassnqg  7333  nqtri3or  7347  lt2addnq  7355  lt2mulnq  7356  enq0ref  7384  enq0tr  7385  nqnq0pi  7389  nqpnq0nq  7404  nqnq0a  7405  distrnq0  7410  addassnq0lemcl  7412  ltsrprg  7698  mulcomsrg  7708  mulasssrg  7709  distrsrg  7710  aptisr  7730  mulcnsr  7786  cnegex  8086  sub4  8153  muladd  8292  ltleadd  8354  divdivdivap  8619  divadddivap  8633  ltmul12a  8765  fzrev  10029  facndiv  10662  cncongr1  12046  blbas  13188  cncfmet  13334  ptolemy  13500