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  5619  fiunsnnn  6895  addcomnqg  7394  addassnqg  7395  nqtri3or  7409  lt2addnq  7417  lt2mulnq  7418  enq0ref  7446  enq0tr  7447  nqnq0pi  7451  nqpnq0nq  7466  nqnq0a  7467  distrnq0  7472  addassnq0lemcl  7474  ltsrprg  7760  mulcomsrg  7770  mulasssrg  7771  distrsrg  7772  aptisr  7792  mulcnsr  7848  cnegex  8149  sub4  8216  muladd  8355  ltleadd  8417  divdivdivap  8684  divadddivap  8698  ltmul12a  8831  fzrev  10098  facndiv  10733  cncongr1  12117  ghmeql  13161  blbas  14286  cncfmet  14432  ptolemy  14598