Theorem 3ad2antl3 1184

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antl3	⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl3

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantll 712	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1163	1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086

This theorem is referenced by:  simpl3  1190  simpl3l  1225  simpl3r  1226  simpl31  1251  simpl32  1252  simpl33  1253  rspc3ev  3618  brcogw  5865  cocan1  7296  ov6g  7582  fpr1  8307  dif1enlem  9179  dif1ennnALT  9300  cfsmolem  10293  coftr  10296  axcc3  10461  axdc4lem  10478  gruf  10834  dedekindle  11408  zdivmul  12664  cshf1  14792  cshimadifsn  14812  fprodle  15972  bpolycl  16028  lcmdvds  16578  lubss  18504  odeq  19509  ghmplusg  19805  lmhmvsca  20934  islindf4  21776  mndifsplit  22556  gsummatr01lem3  22577  gsummatr01  22579  mp2pm2mplem4  22729  elcls  22995  cnpresti  23210  cmpsublem  23321  comppfsc  23454  ptpjcn  23533  elfm3  23872  rnelfmlem  23874  nmoix  24664  caublcls  25255  ig1pdvds  26132  coeid3  26192  amgm  26941  brbtwn2  28760  colinearalg  28765  axsegconlem1  28772  ax5seglem1  28783  ax5seglem2  28784  homco1  31655  hoadddi  31657  br6  35408  lindsenlbs  37145  upixp  37259  filbcmb  37270  3dim1  38996  llni  39037  lplni  39061  lvoli  39104  cdleme42mgN  40017  mzprename  42234  infmrgelbi  42363  relexpxpmin  43212  n0p  44472  rexabslelem  44863  pimxrneun  44934  limcleqr  45095  fnlimfvre  45125  stoweidlem17  45468  stoweidlem28  45479  fourierdlem12  45570  fourierdlem41  45599  fourierdlem42  45600  fourierdlem74  45631  fourierdlem77  45634  qndenserrnopnlem  45748  issalnnd  45796  hspmbllem2  46078  issmfle  46196  smflimlem2  46223  smflimmpt  46261  smfinflem  46268  smflimsuplem7  46277  smflimsupmpt  46280  smfliminfmpt  46283  lighneallem3  47010