Theorem ad2ant2l 499

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 469	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 467	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  mpteqb  5511  mpofun  5873  xpdom2  6725  addcmpblnq  7175  addpipqqslem  7177  addpipqqs  7178  addclnq  7183  addcomnqg  7189  addassnqg  7190  mulcomnqg  7191  mulassnqg  7192  distrnqg  7195  ltdcnq  7205  enq0ref  7241  addcmpblnq0  7251  addclnq0  7259  nqpnq0nq  7261  nqnq0a  7262  nqnq0m  7263  distrnq0  7267  mulcomnq0  7268  addassnq0lemcl  7269  genpdisj  7331  appdiv0nq  7372  addcomsrg  7563  mulcomsrg  7565  mulasssrg  7566  distrsrg  7567  addcnsr  7642  mulcnsr  7643  addcnsrec  7650  axaddcl  7672  axmulcl  7674  axaddcom  7678  add42  7924  muladd  8146  mulsub  8163  apreim  8365  divmuleqap  8477  ltmul12a  8618  lemul12b  8619  lemul12a  8620  qaddcl  9427  qmulcl  9429  iooshf  9735  fzass4  9842  elfzomelpfzo  10008  tanaddaplem  11445  opnneissb  12324  neitx  12437  txcnmpt  12442  txrest  12445  metcnp3  12680  cncfmet  12748  dveflem  12855