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  5655  fiunsnnn  6951  addcomnqg  7467  addassnqg  7468  nqtri3or  7482  lt2addnq  7490  lt2mulnq  7491  enq0ref  7519  enq0tr  7520  nqnq0pi  7524  nqpnq0nq  7539  nqnq0a  7540  distrnq0  7545  addassnq0lemcl  7547  ltsrprg  7833  mulcomsrg  7843  mulasssrg  7844  distrsrg  7845  aptisr  7865  mulcnsr  7921  cnegex  8223  sub4  8290  muladd  8429  ltleadd  8492  divdivdivap  8759  divadddivap  8773  ltmul12a  8906  fzrev  10178  facndiv  10850  cncongr1  12298  ghmeql  13475  blbas  14777  cncfmet  14936  ptolemy  15168