Theorem 3ad2antl3 1187

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 713	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1166	1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpl3  1193  simpl3l  1228  simpl3r  1229  simpl31  1254  simpl32  1255  simpl33  1256  rspc3ev  3652  brcogw  5893  cocan1  7327  ov6g  7614  fpr1  8344  dif1enlem  9222  dif1ennnALT  9339  cfsmolem  10339  coftr  10342  axcc3  10507  axdc4lem  10524  gruf  10880  dedekindle  11454  zdivmul  12715  cshf1  14858  cshimadifsn  14878  fprodle  16044  bpolycl  16100  lcmdvds  16655  lubss  18583  odeq  19592  ghmplusg  19888  lmhmvsca  21067  islindf4  21881  mndifsplit  22663  gsummatr01lem3  22684  gsummatr01  22686  mp2pm2mplem4  22836  elcls  23102  cnpresti  23317  cmpsublem  23428  comppfsc  23561  ptpjcn  23640  elfm3  23979  rnelfmlem  23981  nmoix  24771  caublcls  25362  ig1pdvds  26239  coeid3  26299  amgm  27052  brbtwn2  28938  colinearalg  28943  axsegconlem1  28950  ax5seglem1  28961  ax5seglem2  28962  homco1  31833  hoadddi  31835  br6  35719  lindsenlbs  37575  upixp  37689  filbcmb  37700  3dim1  39424  llni  39465  lplni  39489  lvoli  39532  cdleme42mgN  40445  mzprename  42705  infmrgelbi  42834  relexpxpmin  43679  n0p  44945  rexabslelem  45333  pimxrneun  45404  limcleqr  45565  fnlimfvre  45595  stoweidlem17  45938  stoweidlem28  45949  fourierdlem12  46040  fourierdlem41  46069  fourierdlem42  46070  fourierdlem74  46101  fourierdlem77  46104  qndenserrnopnlem  46218  issalnnd  46266  hspmbllem2  46548  issmfle  46666  smflimlem2  46693  smflimmpt  46731  smfinflem  46738  smflimsuplem7  46747  smflimsupmpt  46750  smfliminfmpt  46753  lighneallem3  47481