Theorem ad2ant2l 512

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  mpteqb  5796  mpofun  6190  xpdom2  7129  addcmpblnq  7735  addpipqqslem  7737  addpipqqs  7738  addclnq  7743  addcomnqg  7749  addassnqg  7750  mulcomnqg  7751  mulassnqg  7752  distrnqg  7755  ltdcnq  7765  enq0ref  7801  addcmpblnq0  7811  addclnq0  7819  nqpnq0nq  7821  nqnq0a  7822  nqnq0m  7823  distrnq0  7827  mulcomnq0  7828  addassnq0lemcl  7829  genpdisj  7891  appdiv0nq  7932  addcomsrg  8123  mulcomsrg  8125  mulasssrg  8126  distrsrg  8127  addcnsr  8202  mulcnsr  8203  addcnsrec  8210  axaddcl  8232  axmulcl  8234  axaddcom  8238  add42  8490  muladd  8713  mulsub  8730  apreim  8934  divmuleqap  9050  ltmul12a  9193  lemul12b  9194  lemul12a  9195  qaddcl  10045  qmulcl  10047  iooshf  10365  fzass4  10479  elfzomelpfzo  10660  swrdccatin2  11517  pfxccatin12  11521  tanaddaplem  12524  issubg4m  14049  ghmpreima  14122  cntzsubg  14165  islmodd  14713  opnneissb  15347  neitx  15460  txcnmpt  15465  txrest  15468  metcnp3  15703  cncfmet  15784  dveflem  15918  efnnfsumcl  16200  efchtqdvds  16226  lgsdir2  16318