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  5682  fiunsnnn  6992  addcomnqg  7509  addassnqg  7510  nqtri3or  7524  lt2addnq  7532  lt2mulnq  7533  enq0ref  7561  enq0tr  7562  nqnq0pi  7566  nqpnq0nq  7581  nqnq0a  7582  distrnq0  7587  addassnq0lemcl  7589  ltsrprg  7875  mulcomsrg  7885  mulasssrg  7886  distrsrg  7887  aptisr  7907  mulcnsr  7963  cnegex  8265  sub4  8332  muladd  8471  ltleadd  8534  divdivdivap  8801  divadddivap  8815  ltmul12a  8948  fzrev  10221  facndiv  10901  cncongr1  12495  ghmeql  13673  blbas  14975  cncfmet  15134  ptolemy  15366