Theorem 3ad2antl1 1184

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

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

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 1088

This theorem is referenced by:  simpl1  1190  simpl1l  1223  simpl1r  1224  simpl11  1247  simpl12  1248  simpl13  1249  smocdmdom  8406  omeulem1  8618  f1oen4g  9003  f1dom4g  9004  dif1ennnALT  9308  ordiso2  9552  infpssrlem4  10343  fin1a2lem9  10445  gchpwdom  10707  tskwun  10821  gruxp  10844  infregelb  12249  fzo1fzo0n0  13750  fsuppmapnn0fiub  14028  pfxsuffeqwrdeq  14732  fprodle  16028  muldvds2  16315  dvds2add  16323  dvds2sub  16324  dvdstr  16327  lcmfledvds  16665  mndvcl  18822  mhmvlin  18826  mulgnnsubcl  19116  mulgpropd  19146  gexdvdsi  19615  ringidss  20290  reslmhm2  21069  obs2ss  21766  lsslindf  21867  issubassa  21904  madurid  22665  restntr  23205  cnpnei  23287  upxp  23646  qtopss  23738  opnfbas  23865  fbasrn  23907  trfg  23914  ufilmax  23930  ustuqtop1  24265  prdsxmetlem  24393  nmoix  24765  nmoi2  24766  iimulcl  24979  mbfimaopn2  25705  lgsval4lem  27366  nodenselem8  27750  f1otrg  28893  brbtwn2  28934  colinearalg  28939  axsegconlem1  28946  0vtxrusgr  29609  clwwlkccatlem  30017  clwwlkccat  30018  clwwisshclwws  30043  clwwlkfo  30078  numclwwlk1lem2fo  30386  lnosub  30787  pjspansn  31605  eulerpartlemb  34349  cnpconn  35214  mclspps  35568  curf  37584  mblfinlem2  37644  mblfinlem3  37645  mettrifi  37743  ghomdiv  37878  grpokerinj  37879  rngohomco  37960  crngohomfo  37992  keridl  38018  cvrcon3b  39258  factwoffsmonot  42223  mzpsubst  42735  lzunuz  42755  diophrex  42762  rmxycomplete  42905  jm2.26  42990  lnmepi  43073  lmhmlnmsplit  43075  nadd2rabex  43375  nadd1rabtr  43377  nadd1rabex  43379  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  uzwo4  44992  wessf1ornlem  45127  choicefi  45142  supxrgere  45282  supxrgelem  45286  supxrge  45287  suplesup  45288  infxr  45316  infleinflem2  45320  rexabslelem  45367  fmul01lt1  45541  limcleqr  45599  limclner  45606  dvnprodlem1  45901  volioc  45927  stoweidlem60  46015  wallispilem3  46022  fourierdlem12  46074  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem54  46115  fourierdlem68  46129  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem83  46144  elaa2  46189  etransclem24  46213  etransclem32  46221  ioorrnopnlem  46259  issalnnd  46300  sge0xaddlem2  46389  sge0seq  46401  meaiininc2  46443  hoicvr  46503  ovnsubaddlem2  46526  hoidmvval0  46542  hoidmvlelem3  46552  hspmbllem2  46582  vonioo  46637  vonicc  46640  smfinflem  46772  fsupdm  46797  finfdm  46801  fmtnoprmfac2lem1  47490  fmtnofac1  47494  lincresunit3lem3  48319  suppdm  48355  inlinecirc02p  48636