Theorem 3ad2antl1 1204

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl1  1210  simpl1l  1243  simpl1r  1244  simpl11  1267  simpl12  1268  simpl13  1269  smocdmdom  8377  omeulem1  8591  curf  8891  f1oen4g  8992  f1dom4g  8993  dif1ennnALT  9269  ordiso2  9510  infpssrlem4  10385  fin1a2lem9  10487  gchpwdom  10756  tskwun  10870  gruxp  10893  infregelb  12302  fzo1fzo0n0  13851  fsuppmapnn0fiub  14135  pfxsuffeqwrdeq  14848  fprodle  16164  muldvds2  16452  dvds2add  16461  dvds2sub  16462  dvdstr  16465  lcmfledvds  16808  mndvcl  18993  mhmvlin  18997  mulgnnsubcl  19297  mulgpropd  19327  gexdvdsi  19798  ringidss  20507  reslmhm2  21329  obs2ss  22036  lsslindf  22137  issubassa  22176  madurid  22960  restntr  23501  cnpnei  23583  upxp  23943  qtopss  24035  opnfbas  24162  fbasrn  24204  trfg  24211  ufilmax  24227  ustuqtop1  24561  prdsxmetlem  24688  nmoix  25049  nmoi2  25050  iimulcl  25259  mbfimaopn2  25979  lgsval4lem  27636  nodenselem8  28049  f1otrg  29449  brbtwn2  29484  colinearalg  29489  axsegconlem1  29496  0vtxrusgr  30159  clwwlkccatlem  30581  clwwlkccat  30582  clwwisshclwws  30607  clwwlkfo  30642  numclwwlk1lem2fo  30960  lnosub  31362  pjspansn  32180  eulerpartlemb  35001  cnpconn  35996  mclspps  36350  mblfinlem2  38578  mblfinlem3  38579  mettrifi  38693  ghomdiv  38828  grpokerinj  38829  rngohomco  38910  crngohomfo  38942  keridl  38968  cvrcon3b  40336  mzpsubst  43760  lzunuz  43780  diophrex  43787  rmxycomplete  43925  jm2.26  44010  lnmepi  44088  lmhmlnmsplit  44090  nadd2rabex  44389  nadd1rabtr  44391  nadd1rabex  44393  ntrclsiso  45068  ntrclskb  45070  ntrclsk3  45071  uzwo4  46071  wessf1ornlem  46201  choicefi  46215  supxrgere  46346  supxrgelem  46350  supxrge  46351  suplesup  46352  infxr  46379  infleinflem2  46383  rexabslelem  46429  fmul01lt1  46599  limcleqr  46655  limclner  46662  dvnprodlem1  46957  volioc  46983  stoweidlem60  47071  wallispilem3  47078  fourierdlem12  47130  fourierdlem41  47159  fourierdlem42  47160  fourierdlem48  47165  fourierdlem49  47166  fourierdlem54  47171  fourierdlem68  47185  fourierdlem73  47190  fourierdlem74  47191  fourierdlem75  47192  fourierdlem83  47200  elaa2  47245  etransclem24  47269  etransclem32  47277  ioorrnopnlem  47315  issalnnd  47356  sge0xaddlem2  47445  sge0seq  47457  meaiininc2  47499  hoicvr  47559  ovnsubaddlem2  47582  hoidmvval0  47598  hoidmvlelem3  47608  hspmbllem2  47638  vonioo  47693  vonicc  47696  smfinflem  47828  fsupdm  47853  finfdm  47857  fmtnoprmfac2lem1  48652  fmtnofac1  48656  lincresunit3lem3  49587  suppdm  49623  inlinecirc02p  49900