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  5733  mpofun  6118  xpdom2  7010  addcmpblnq  7577  addpipqqslem  7579  addpipqqs  7580  addclnq  7585  addcomnqg  7591  addassnqg  7592  mulcomnqg  7593  mulassnqg  7594  distrnqg  7597  ltdcnq  7607  enq0ref  7643  addcmpblnq0  7653  addclnq0  7661  nqpnq0nq  7663  nqnq0a  7664  nqnq0m  7665  distrnq0  7669  mulcomnq0  7670  addassnq0lemcl  7671  genpdisj  7733  appdiv0nq  7774  addcomsrg  7965  mulcomsrg  7967  mulasssrg  7968  distrsrg  7969  addcnsr  8044  mulcnsr  8045  addcnsrec  8052  axaddcl  8074  axmulcl  8076  axaddcom  8080  add42  8331  muladd  8553  mulsub  8570  apreim  8773  divmuleqap  8887  ltmul12a  9030  lemul12b  9031  lemul12a  9032  qaddcl  9859  qmulcl  9861  iooshf  10177  fzass4  10287  elfzomelpfzo  10466  swrdccatin2  11300  pfxccatin12  11304  tanaddaplem  12289  issubg4m  13770  ghmpreima  13843  islmodd  14297  opnneissb  14869  neitx  14982  txcnmpt  14987  txrest  14990  metcnp3  15225  cncfmet  15306  dveflem  15440  lgsdir2  15752