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  5608  mpofun  5979  xpdom2  6833  addcmpblnq  7368  addpipqqslem  7370  addpipqqs  7371  addclnq  7376  addcomnqg  7382  addassnqg  7383  mulcomnqg  7384  mulassnqg  7385  distrnqg  7388  ltdcnq  7398  enq0ref  7434  addcmpblnq0  7444  addclnq0  7452  nqpnq0nq  7454  nqnq0a  7455  nqnq0m  7456  distrnq0  7460  mulcomnq0  7461  addassnq0lemcl  7462  genpdisj  7524  appdiv0nq  7565  addcomsrg  7756  mulcomsrg  7758  mulasssrg  7759  distrsrg  7760  addcnsr  7835  mulcnsr  7836  addcnsrec  7843  axaddcl  7865  axmulcl  7867  axaddcom  7871  add42  8121  muladd  8343  mulsub  8360  apreim  8562  divmuleqap  8676  ltmul12a  8819  lemul12b  8820  lemul12a  8821  qaddcl  9637  qmulcl  9639  iooshf  9954  fzass4  10064  elfzomelpfzo  10233  tanaddaplem  11748  issubg4m  13058  islmodd  13388  opnneissb  13740  neitx  13853  txcnmpt  13858  txrest  13861  metcnp3  14096  cncfmet  14164  dveflem  14272  lgsdir2  14519