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  5724  mpofun  6105  xpdom2  6986  addcmpblnq  7550  addpipqqslem  7552  addpipqqs  7553  addclnq  7558  addcomnqg  7564  addassnqg  7565  mulcomnqg  7566  mulassnqg  7567  distrnqg  7570  ltdcnq  7580  enq0ref  7616  addcmpblnq0  7626  addclnq0  7634  nqpnq0nq  7636  nqnq0a  7637  nqnq0m  7638  distrnq0  7642  mulcomnq0  7643  addassnq0lemcl  7644  genpdisj  7706  appdiv0nq  7747  addcomsrg  7938  mulcomsrg  7940  mulasssrg  7941  distrsrg  7942  addcnsr  8017  mulcnsr  8018  addcnsrec  8025  axaddcl  8047  axmulcl  8049  axaddcom  8053  add42  8304  muladd  8526  mulsub  8543  apreim  8746  divmuleqap  8860  ltmul12a  9003  lemul12b  9004  lemul12a  9005  qaddcl  9826  qmulcl  9828  iooshf  10144  fzass4  10254  elfzomelpfzo  10432  swrdccatin2  11256  pfxccatin12  11260  tanaddaplem  12244  issubg4m  13725  ghmpreima  13798  islmodd  14251  opnneissb  14823  neitx  14936  txcnmpt  14941  txrest  14944  metcnp3  15179  cncfmet  15260  dveflem  15394  lgsdir2  15706