Theorem ad2ant2lr 502

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 471	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 468	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  5519  fiunsnnn  6783  addcomnqg  7213  addassnqg  7214  nqtri3or  7228  lt2addnq  7236  lt2mulnq  7237  enq0ref  7265  enq0tr  7266  nqnq0pi  7270  nqpnq0nq  7285  nqnq0a  7286  distrnq0  7291  addassnq0lemcl  7293  ltsrprg  7579  mulcomsrg  7589  mulasssrg  7590  distrsrg  7591  aptisr  7611  mulcnsr  7667  cnegex  7964  sub4  8031  muladd  8170  ltleadd  8232  divdivdivap  8497  divadddivap  8511  ltmul12a  8642  fzrev  9895  facndiv  10517  cncongr1  11820  blbas  12641  cncfmet  12787  ptolemy  12953