Theorem ad2ant2l 500

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2l	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 470	. 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  5557  mpofun  5920  xpdom2  6773  addcmpblnq  7281  addpipqqslem  7283  addpipqqs  7284  addclnq  7289  addcomnqg  7295  addassnqg  7296  mulcomnqg  7297  mulassnqg  7298  distrnqg  7301  ltdcnq  7311  enq0ref  7347  addcmpblnq0  7357  addclnq0  7365  nqpnq0nq  7367  nqnq0a  7368  nqnq0m  7369  distrnq0  7373  mulcomnq0  7374  addassnq0lemcl  7375  genpdisj  7437  appdiv0nq  7478  addcomsrg  7669  mulcomsrg  7671  mulasssrg  7672  distrsrg  7673  addcnsr  7748  mulcnsr  7749  addcnsrec  7756  axaddcl  7778  axmulcl  7780  axaddcom  7784  add42  8031  muladd  8253  mulsub  8270  apreim  8472  divmuleqap  8584  ltmul12a  8725  lemul12b  8726  lemul12a  8727  qaddcl  9537  qmulcl  9539  iooshf  9849  fzass4  9957  elfzomelpfzo  10123  tanaddaplem  11628  opnneissb  12526  neitx  12639  txcnmpt  12644  txrest  12647  metcnp3  12882  cncfmet  12950  dveflem  13058