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  5695  mpofun  6072  xpdom2  6953  addcmpblnq  7517  addpipqqslem  7519  addpipqqs  7520  addclnq  7525  addcomnqg  7531  addassnqg  7532  mulcomnqg  7533  mulassnqg  7534  distrnqg  7537  ltdcnq  7547  enq0ref  7583  addcmpblnq0  7593  addclnq0  7601  nqpnq0nq  7603  nqnq0a  7604  nqnq0m  7605  distrnq0  7609  mulcomnq0  7610  addassnq0lemcl  7611  genpdisj  7673  appdiv0nq  7714  addcomsrg  7905  mulcomsrg  7907  mulasssrg  7908  distrsrg  7909  addcnsr  7984  mulcnsr  7985  addcnsrec  7992  axaddcl  8014  axmulcl  8016  axaddcom  8020  add42  8271  muladd  8493  mulsub  8510  apreim  8713  divmuleqap  8827  ltmul12a  8970  lemul12b  8971  lemul12a  8972  qaddcl  9793  qmulcl  9795  iooshf  10111  fzass4  10221  elfzomelpfzo  10399  swrdccatin2  11222  pfxccatin12  11226  tanaddaplem  12210  issubg4m  13690  ghmpreima  13763  islmodd  14216  opnneissb  14788  neitx  14901  txcnmpt  14906  txrest  14909  metcnp3  15144  cncfmet  15225  dveflem  15359  lgsdir2  15671