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  8384  omeulem1  8598  curf  8898  f1oen4g  8999  f1dom4g  9000  dif1ennnALT  9276  ordiso2  9516  infpssrlem4  10391  fin1a2lem9  10493  gchpwdom  10762  tskwun  10876  gruxp  10899  infregelb  12308  fzo1fzo0n0  13857  fsuppmapnn0fiub  14141  pfxsuffeqwrdeq  14855  fprodle  16172  muldvds2  16460  dvds2add  16469  dvds2sub  16470  dvdstr  16473  lcmfledvds  16816  mndvcl  19001  mhmvlin  19005  mulgnnsubcl  19305  mulgpropd  19335  gexdvdsi  19806  ringidss  20515  reslmhm2  21337  obs2ss  22044  lsslindf  22145  issubassa  22184  madurid  22968  restntr  23509  cnpnei  23591  upxp  23951  qtopss  24043  opnfbas  24170  fbasrn  24212  trfg  24219  ufilmax  24235  ustuqtop1  24569  prdsxmetlem  24696  nmoix  25057  nmoi2  25058  iimulcl  25267  mbfimaopn2  25987  lgsval4lem  27644  nodenselem8  28057  f1otrg  29457  brbtwn2  29492  colinearalg  29497  axsegconlem1  29504  0vtxrusgr  30167  clwwlkccatlem  30589  clwwlkccat  30590  clwwisshclwws  30615  clwwlkfo  30650  numclwwlk1lem2fo  30968  lnosub  31370  pjspansn  32188  eulerpartlemb  35050  cnpconn  36113  mclspps  36467  mblfinlem2  38713  mblfinlem3  38714  mettrifi  38828  ghomdiv  38963  grpokerinj  38964  rngohomco  39045  crngohomfo  39077  keridl  39103  cvrcon3b  40471  mzpsubst  43896  lzunuz  43916  diophrex  43923  rmxycomplete  44061  jm2.26  44146  lnmepi  44224  lmhmlnmsplit  44226  nadd2rabex  44525  nadd1rabtr  44527  nadd1rabex  44529  ntrclsiso  45204  ntrclskb  45206  ntrclsk3  45207  uzwo4  46206  wessf1ornlem  46336  choicefi  46350  supxrgere  46481  supxrgelem  46485  supxrge  46486  suplesup  46487  infxr  46514  infleinflem2  46518  rexabslelem  46564  fmul01lt1  46734  limcleqr  46790  limclner  46797  dvnprodlem1  47092  volioc  47118  stoweidlem60  47206  wallispilem3  47213  fourierdlem12  47265  fourierdlem41  47294  fourierdlem42  47295  fourierdlem48  47300  fourierdlem49  47301  fourierdlem54  47306  fourierdlem68  47320  fourierdlem73  47325  fourierdlem74  47326  fourierdlem75  47327  fourierdlem83  47335  elaa2  47380  etransclem24  47404  etransclem32  47412  ioorrnopnlem  47450  issalnnd  47491  sge0xaddlem2  47580  sge0seq  47592  meaiininc2  47634  hoicvr  47694  ovnsubaddlem2  47717  hoidmvval0  47733  hoidmvlelem3  47743  hspmbllem2  47773  vonioo  47828  vonicc  47831  smfinflem  47963  fsupdm  47988  finfdm  47992  fmtnoprmfac2lem1  48787  fmtnofac1  48791  lincresunit3lem3  49722  suppdm  49758  inlinecirc02p  50035