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  8358  omeulem1  8570  curf  8870  f1oen4g  8971  f1dom4g  8972  dif1ennnALT  9248  ordiso2  9488  infpssrlem4  10309  fin1a2lem9  10411  gchpwdom  10680  tskwun  10794  gruxp  10817  infregelb  12224  fzo1fzo0n0  13772  fsuppmapnn0fiub  14056  pfxsuffeqwrdeq  14768  fprodle  16084  muldvds2  16372  dvds2add  16381  dvds2sub  16382  dvdstr  16385  lcmfledvds  16723  mndvcl  18906  mhmvlin  18910  mulgnnsubcl  19210  mulgpropd  19240  gexdvdsi  19711  ringidss  20419  reslmhm2  21238  obs2ss  21943  lsslindf  22044  issubassa  22083  madurid  22867  restntr  23408  cnpnei  23490  upxp  23850  qtopss  23942  opnfbas  24069  fbasrn  24111  trfg  24118  ufilmax  24134  ustuqtop1  24468  prdsxmetlem  24595  nmoix  24956  nmoi2  24957  iimulcl  25166  mbfimaopn2  25886  lgsval4lem  27545  nodenselem8  27928  f1otrg  29328  brbtwn2  29363  colinearalg  29368  axsegconlem1  29375  0vtxrusgr  30038  clwwlkccatlem  30460  clwwlkccat  30461  clwwisshclwws  30486  clwwlkfo  30521  numclwwlk1lem2fo  30839  lnosub  31241  pjspansn  32059  eulerpartlemb  34880  cnpconn  35810  mclspps  36164  mblfinlem2  38408  mblfinlem3  38409  mettrifi  38508  ghomdiv  38643  grpokerinj  38644  rngohomco  38725  crngohomfo  38757  keridl  38783  cvrcon3b  40151  mzpsubst  43594  lzunuz  43614  diophrex  43621  rmxycomplete  43759  jm2.26  43844  lnmepi  43927  lmhmlnmsplit  43929  nadd2rabex  44228  nadd1rabtr  44230  nadd1rabex  44232  ntrclsiso  44908  ntrclskb  44910  ntrclsk3  44911  uzwo4  45888  wessf1ornlem  46018  choicefi  46032  supxrgere  46164  supxrgelem  46168  supxrge  46169  suplesup  46170  infxr  46197  infleinflem2  46201  rexabslelem  46247  fmul01lt1  46417  limcleqr  46473  limclner  46480  dvnprodlem1  46775  volioc  46801  stoweidlem60  46889  wallispilem3  46896  fourierdlem12  46948  fourierdlem41  46977  fourierdlem42  46978  fourierdlem48  46983  fourierdlem49  46984  fourierdlem54  46989  fourierdlem68  47003  fourierdlem73  47008  fourierdlem74  47009  fourierdlem75  47010  fourierdlem83  47018  elaa2  47063  etransclem24  47087  etransclem32  47095  ioorrnopnlem  47133  issalnnd  47174  sge0xaddlem2  47263  sge0seq  47275  meaiininc2  47317  hoicvr  47377  ovnsubaddlem2  47400  hoidmvval0  47416  hoidmvlelem3  47426  hspmbllem2  47456  vonioo  47511  vonicc  47514  smfinflem  47646  fsupdm  47671  finfdm  47675  fmtnoprmfac2lem1  48470  fmtnofac1  48474  lincresunit3lem3  49405  suppdm  49441  inlinecirc02p  49718