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  5655  mpofun  6028  xpdom2  6899  addcmpblnq  7453  addpipqqslem  7455  addpipqqs  7456  addclnq  7461  addcomnqg  7467  addassnqg  7468  mulcomnqg  7469  mulassnqg  7470  distrnqg  7473  ltdcnq  7483  enq0ref  7519  addcmpblnq0  7529  addclnq0  7537  nqpnq0nq  7539  nqnq0a  7540  nqnq0m  7541  distrnq0  7545  mulcomnq0  7546  addassnq0lemcl  7547  genpdisj  7609  appdiv0nq  7650  addcomsrg  7841  mulcomsrg  7843  mulasssrg  7844  distrsrg  7845  addcnsr  7920  mulcnsr  7921  addcnsrec  7928  axaddcl  7950  axmulcl  7952  axaddcom  7956  add42  8207  muladd  8429  mulsub  8446  apreim  8649  divmuleqap  8763  ltmul12a  8906  lemul12b  8907  lemul12a  8908  qaddcl  9728  qmulcl  9730  iooshf  10046  fzass4  10156  elfzomelpfzo  10326  tanaddaplem  11922  issubg4m  13401  ghmpreima  13474  islmodd  13927  opnneissb  14499  neitx  14612  txcnmpt  14617  txrest  14620  metcnp3  14855  cncfmet  14936  dveflem  15070  lgsdir2  15382