Theorem 3ad2antl1 1185

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 1167	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpl1  1191  simpl1l  1224  simpl1r  1225  simpl11  1248  simpl12  1249  simpl13  1250  smocdmdom  8319  omeulem1  8534  f1oen4g  8911  f1dom4g  8912  dif1ennnALT  9228  ordiso2  9460  infpssrlem4  10251  fin1a2lem9  10353  gchpwdom  10615  tskwun  10729  gruxp  10752  infregelb  12148  fzo1fzo0n0  13633  fsuppmapnn0fiub  13906  pfxsuffeqwrdeq  14598  fprodle  15890  muldvds2  16175  dvds2add  16183  dvds2sub  16184  dvdstr  16187  lcmfledvds  16519  mulgnnsubcl  18902  mulgpropd  18932  gexdvdsi  19379  ringidss  20012  reslmhm2  20571  obs2ss  21172  lsslindf  21273  issubassa  21309  mndvcl  21777  mhmvlin  21783  madurid  22030  restntr  22570  cnpnei  22652  upxp  23011  qtopss  23103  opnfbas  23230  fbasrn  23272  trfg  23279  ufilmax  23295  ustuqtop1  23630  prdsxmetlem  23758  nmoix  24130  nmoi2  24131  iimulcl  24337  mbfimaopn2  25058  lgsval4lem  26693  nodenselem8  27076  f1otrg  27876  brbtwn2  27917  colinearalg  27922  axsegconlem1  27929  0vtxrusgr  28588  clwwlkccatlem  28996  clwwlkccat  28997  clwwisshclwws  29022  clwwlkfo  29057  numclwwlk1lem2fo  29365  lnosub  29764  pjspansn  30582  eulerpartlemb  33057  cnpconn  33911  mclspps  34265  curf  36129  mblfinlem2  36189  mblfinlem3  36190  mettrifi  36289  ghomdiv  36424  grpokerinj  36425  rngohomco  36506  crngohomfo  36538  keridl  36564  cvrcon3b  37812  factwoffsmonot  40688  mzpsubst  41129  lzunuz  41149  diophrex  41156  rmxycomplete  41299  jm2.26  41384  lnmepi  41470  lmhmlnmsplit  41472  nadd2rabex  41779  nadd1rabtr  41781  nadd1rabex  41783  ntrclsiso  42461  ntrclskb  42463  ntrclsk3  42464  uzwo4  43383  wessf1ornlem  43525  choicefi  43542  supxrgere  43688  supxrgelem  43692  supxrge  43693  suplesup  43694  infxr  43722  infleinflem2  43726  rexabslelem  43773  fmul01lt1  43947  limcleqr  44005  limclner  44012  dvnprodlem1  44307  volioc  44333  stoweidlem60  44421  wallispilem3  44428  fourierdlem12  44480  fourierdlem41  44509  fourierdlem42  44510  fourierdlem48  44515  fourierdlem49  44516  fourierdlem54  44521  fourierdlem68  44535  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem83  44550  elaa2  44595  etransclem24  44619  etransclem32  44627  ioorrnopnlem  44665  issalnnd  44706  sge0xaddlem2  44795  sge0seq  44807  meaiininc2  44849  hoicvr  44909  ovnsubaddlem2  44932  hoidmvval0  44948  hoidmvlelem3  44958  hspmbllem2  44988  vonioo  45043  vonicc  45046  smfinflem  45178  fsupdm  45203  finfdm  45207  fmtnoprmfac2lem1  45878  fmtnofac1  45882  lincresunit3lem3  46675  suppdm  46711  inlinecirc02p  46993