Theorem 3ad2antl1 1181

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 713	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1163	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpl1  1187  simpl1l  1220  simpl1r  1221  simpl11  1244  simpl12  1245  simpl13  1246  smorndom  8007  omeulem1  8210  dif1en  8753  ordiso2  8981  infpssrlem4  9730  fin1a2lem9  9832  gchpwdom  10094  tskwun  10208  gruxp  10231  infregelb  11627  fzo1fzo0n0  13091  fsuppmapnn0fiub  13362  ccat2s1fvwOLD  14001  pfxsuffeqwrdeq  14062  fprodle  15352  muldvds2  15637  dvds2add  15645  dvds2sub  15646  dvdstr  15648  lcmfledvds  15978  mulgnnsubcl  18242  mulgpropd  18271  gexdvdsi  18710  ringidss  19329  reslmhm2  19827  issubassa  20100  obs2ss  20875  lsslindf  20976  mndvcl  21004  mhmvlin  21010  madurid  21255  restntr  21792  cnpnei  21874  upxp  22233  qtopss  22325  opnfbas  22452  fbasrn  22494  trfg  22501  ufilmax  22517  ustuqtop1  22852  prdsxmetlem  22980  nmoix  23340  nmoi2  23341  iimulcl  23543  mbfimaopn2  24260  lgsval4lem  25886  f1otrg  26659  brbtwn2  26693  colinearalg  26698  axsegconlem1  26705  0vtxrusgr  27361  clwwlkccatlem  27769  clwwlkccat  27770  clwwisshclwws  27795  clwwlkfo  27831  numclwwlk1lem2fo  28139  lnosub  28538  pjspansn  29356  eulerpartlemb  31628  cnpconn  32479  mclspps  32833  nodenselem8  33197  curf  34872  mblfinlem2  34932  mblfinlem3  34933  mettrifi  35034  ghomdiv  35172  grpokerinj  35173  rngohomco  35254  crngohomfo  35286  keridl  35312  cvrcon3b  36415  factwoffsmonot  39105  mzpsubst  39352  lzunuz  39372  diophrex  39379  rmxycomplete  39521  jm2.26  39606  lnmepi  39692  lmhmlnmsplit  39694  ntrclsiso  40424  ntrclskb  40426  ntrclsk3  40427  uzwo4  41322  wessf1ornlem  41452  choicefi  41470  supxrgere  41608  supxrgelem  41612  supxrge  41613  suplesup  41614  infxr  41642  infleinflem2  41646  rexabslelem  41699  fmul01lt1  41874  limcleqr  41932  limclner  41939  dvnprodlem1  42238  volioc  42264  stoweidlem60  42352  wallispilem3  42359  fourierdlem12  42411  fourierdlem41  42440  fourierdlem42  42441  fourierdlem48  42446  fourierdlem49  42447  fourierdlem54  42452  fourierdlem68  42466  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem83  42481  elaa2  42526  etransclem24  42550  etransclem32  42558  ioorrnopnlem  42596  issalnnd  42635  sge0xaddlem2  42723  sge0seq  42735  meaiininc2  42777  hoicvr  42837  ovnsubaddlem2  42860  hoidmvval0  42876  hoidmvlelem3  42886  hspmbllem2  42916  vonioo  42971  vonicc  42974  smfinflem  43098  fmtnoprmfac2lem1  43735  fmtnofac1  43739  lincresunit3lem3  44536  suppdm  44572  inlinecirc02p  44781