Theorem ad2ant2l 508

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 478	. 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  5670  mpofun  6047  xpdom2  6926  addcmpblnq  7480  addpipqqslem  7482  addpipqqs  7483  addclnq  7488  addcomnqg  7494  addassnqg  7495  mulcomnqg  7496  mulassnqg  7497  distrnqg  7500  ltdcnq  7510  enq0ref  7546  addcmpblnq0  7556  addclnq0  7564  nqpnq0nq  7566  nqnq0a  7567  nqnq0m  7568  distrnq0  7572  mulcomnq0  7573  addassnq0lemcl  7574  genpdisj  7636  appdiv0nq  7677  addcomsrg  7868  mulcomsrg  7870  mulasssrg  7871  distrsrg  7872  addcnsr  7947  mulcnsr  7948  addcnsrec  7955  axaddcl  7977  axmulcl  7979  axaddcom  7983  add42  8234  muladd  8456  mulsub  8473  apreim  8676  divmuleqap  8790  ltmul12a  8933  lemul12b  8934  lemul12a  8935  qaddcl  9756  qmulcl  9758  iooshf  10074  fzass4  10184  elfzomelpfzo  10360  tanaddaplem  12049  issubg4m  13529  ghmpreima  13602  islmodd  14055  opnneissb  14627  neitx  14740  txcnmpt  14745  txrest  14748  metcnp3  14983  cncfmet  15064  dveflem  15198  lgsdir2  15510