Theorem 3ad2antl1 1182

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 714	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1164	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpl1  1188  simpl1l  1221  simpl1r  1222  simpl11  1245  simpl12  1246  simpl13  1247  smorndom  7988  omeulem1  8191  dif1en  8735  ordiso2  8963  infpssrlem4  9717  fin1a2lem9  9819  gchpwdom  10081  tskwun  10195  gruxp  10218  infregelb  11612  fzo1fzo0n0  13083  fsuppmapnn0fiub  13354  ccat2s1fvwOLD  13990  pfxsuffeqwrdeq  14051  fprodle  15342  muldvds2  15627  dvds2add  15635  dvds2sub  15636  dvdstr  15638  lcmfledvds  15966  mulgnnsubcl  18232  mulgpropd  18261  gexdvdsi  18700  ringidss  19323  reslmhm2  19818  obs2ss  20418  lsslindf  20519  issubassa  20555  mndvcl  20998  mhmvlin  21004  madurid  21249  restntr  21787  cnpnei  21869  upxp  22228  qtopss  22320  opnfbas  22447  fbasrn  22489  trfg  22496  ufilmax  22512  ustuqtop1  22847  prdsxmetlem  22975  nmoix  23335  nmoi2  23336  iimulcl  23542  mbfimaopn2  24261  lgsval4lem  25892  f1otrg  26665  brbtwn2  26699  colinearalg  26704  axsegconlem1  26711  0vtxrusgr  27367  clwwlkccatlem  27774  clwwlkccat  27775  clwwisshclwws  27800  clwwlkfo  27835  numclwwlk1lem2fo  28143  lnosub  28542  pjspansn  29360  eulerpartlemb  31736  cnpconn  32590  mclspps  32944  nodenselem8  33308  curf  35035  mblfinlem2  35095  mblfinlem3  35096  mettrifi  35195  ghomdiv  35330  grpokerinj  35331  rngohomco  35412  crngohomfo  35444  keridl  35470  cvrcon3b  36573  factwoffsmonot  39388  mzpsubst  39689  lzunuz  39709  diophrex  39716  rmxycomplete  39858  jm2.26  39943  lnmepi  40029  lmhmlnmsplit  40031  ntrclsiso  40770  ntrclskb  40772  ntrclsk3  40773  uzwo4  41687  wessf1ornlem  41811  choicefi  41829  supxrgere  41965  supxrgelem  41969  supxrge  41970  suplesup  41971  infxr  41999  infleinflem2  42003  rexabslelem  42055  fmul01lt1  42228  limcleqr  42286  limclner  42293  dvnprodlem1  42588  volioc  42614  stoweidlem60  42702  wallispilem3  42709  fourierdlem12  42761  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem54  42802  fourierdlem68  42816  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem83  42831  elaa2  42876  etransclem24  42900  etransclem32  42908  ioorrnopnlem  42946  issalnnd  42985  sge0xaddlem2  43073  sge0seq  43085  meaiininc2  43127  hoicvr  43187  ovnsubaddlem2  43210  hoidmvval0  43226  hoidmvlelem3  43236  hspmbllem2  43266  vonioo  43321  vonicc  43324  smfinflem  43448  fmtnoprmfac2lem1  44083  fmtnofac1  44087  lincresunit3lem3  44883  suppdm  44919  inlinecirc02p  45201