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  5669  mpofun  6046  xpdom2  6925  addcmpblnq  7479  addpipqqslem  7481  addpipqqs  7482  addclnq  7487  addcomnqg  7493  addassnqg  7494  mulcomnqg  7495  mulassnqg  7496  distrnqg  7499  ltdcnq  7509  enq0ref  7545  addcmpblnq0  7555  addclnq0  7563  nqpnq0nq  7565  nqnq0a  7566  nqnq0m  7567  distrnq0  7571  mulcomnq0  7572  addassnq0lemcl  7573  genpdisj  7635  appdiv0nq  7676  addcomsrg  7867  mulcomsrg  7869  mulasssrg  7870  distrsrg  7871  addcnsr  7946  mulcnsr  7947  addcnsrec  7954  axaddcl  7976  axmulcl  7978  axaddcom  7982  add42  8233  muladd  8455  mulsub  8472  apreim  8675  divmuleqap  8789  ltmul12a  8932  lemul12b  8933  lemul12a  8934  qaddcl  9755  qmulcl  9757  iooshf  10073  fzass4  10183  elfzomelpfzo  10358  tanaddaplem  12020  issubg4m  13500  ghmpreima  13573  islmodd  14026  opnneissb  14598  neitx  14711  txcnmpt  14716  txrest  14719  metcnp3  14954  cncfmet  15035  dveflem  15169  lgsdir2  15481