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  5737  mpofun  6122  xpdom2  7014  addcmpblnq  7586  addpipqqslem  7588  addpipqqs  7589  addclnq  7594  addcomnqg  7600  addassnqg  7601  mulcomnqg  7602  mulassnqg  7603  distrnqg  7606  ltdcnq  7616  enq0ref  7652  addcmpblnq0  7662  addclnq0  7670  nqpnq0nq  7672  nqnq0a  7673  nqnq0m  7674  distrnq0  7678  mulcomnq0  7679  addassnq0lemcl  7680  genpdisj  7742  appdiv0nq  7783  addcomsrg  7974  mulcomsrg  7976  mulasssrg  7977  distrsrg  7978  addcnsr  8053  mulcnsr  8054  addcnsrec  8061  axaddcl  8083  axmulcl  8085  axaddcom  8089  add42  8340  muladd  8562  mulsub  8579  apreim  8782  divmuleqap  8896  ltmul12a  9039  lemul12b  9040  lemul12a  9041  qaddcl  9868  qmulcl  9870  iooshf  10186  fzass4  10296  elfzomelpfzo  10475  swrdccatin2  11309  pfxccatin12  11313  tanaddaplem  12298  issubg4m  13779  ghmpreima  13852  islmodd  14306  opnneissb  14878  neitx  14991  txcnmpt  14996  txrest  14999  metcnp3  15234  cncfmet  15315  dveflem  15449  lgsdir2  15761