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  5746  mpofun  6133  xpdom2  7058  addcmpblnq  7630  addpipqqslem  7632  addpipqqs  7633  addclnq  7638  addcomnqg  7644  addassnqg  7645  mulcomnqg  7646  mulassnqg  7647  distrnqg  7650  ltdcnq  7660  enq0ref  7696  addcmpblnq0  7706  addclnq0  7714  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  distrnq0  7722  mulcomnq0  7723  addassnq0lemcl  7724  genpdisj  7786  appdiv0nq  7827  addcomsrg  8018  mulcomsrg  8020  mulasssrg  8021  distrsrg  8022  addcnsr  8097  mulcnsr  8098  addcnsrec  8105  axaddcl  8127  axmulcl  8129  axaddcom  8133  add42  8383  muladd  8605  mulsub  8622  apreim  8825  divmuleqap  8939  ltmul12a  9082  lemul12b  9083  lemul12a  9084  qaddcl  9913  qmulcl  9915  iooshf  10231  fzass4  10342  elfzomelpfzo  10522  swrdccatin2  11359  pfxccatin12  11363  tanaddaplem  12362  issubg4m  13843  ghmpreima  13916  islmodd  14372  opnneissb  14949  neitx  15062  txcnmpt  15067  txrest  15070  metcnp3  15305  cncfmet  15386  dveflem  15520  lgsdir2  15835