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  8361  omeulem1  8573  f1oen4g  8967  f1dom4g  8968  dif1ennnALT  9244  ordiso2  9484  infpssrlem4  10305  fin1a2lem9  10407  gchpwdom  10672  tskwun  10786  gruxp  10809  infregelb  12216  fzo1fzo0n0  13763  fsuppmapnn0fiub  14047  pfxsuffeqwrdeq  14759  fprodle  16075  muldvds2  16363  dvds2add  16372  dvds2sub  16373  dvdstr  16376  lcmfledvds  16714  mndvcl  18894  mhmvlin  18898  mulgnnsubcl  19198  mulgpropd  19228  gexdvdsi  19699  ringidss  20407  reslmhm2  21226  obs2ss  21931  lsslindf  22032  issubassa  22069  madurid  22853  restntr  23391  cnpnei  23473  upxp  23833  qtopss  23925  opnfbas  24052  fbasrn  24094  trfg  24101  ufilmax  24117  ustuqtop1  24451  prdsxmetlem  24578  nmoix  24939  nmoi2  24940  iimulcl  25149  mbfimaopn2  25869  lgsval4lem  27525  nodenselem8  27908  f1otrg  29277  brbtwn2  29312  colinearalg  29317  axsegconlem1  29324  0vtxrusgr  29987  clwwlkccatlem  30409  clwwlkccat  30410  clwwisshclwws  30435  clwwlkfo  30470  numclwwlk1lem2fo  30782  lnosub  31184  pjspansn  32002  eulerpartlemb  34825  cnpconn  35761  mclspps  36115  curf  38308  mblfinlem2  38368  mblfinlem3  38369  mettrifi  38468  ghomdiv  38603  grpokerinj  38604  rngohomco  38685  crngohomfo  38717  keridl  38743  cvrcon3b  40111  mzpsubst  43539  lzunuz  43559  diophrex  43566  rmxycomplete  43704  jm2.26  43789  lnmepi  43872  lmhmlnmsplit  43874  nadd2rabex  44173  nadd1rabtr  44175  nadd1rabex  44177  ntrclsiso  44853  ntrclskb  44855  ntrclsk3  44856  uzwo4  45833  wessf1ornlem  45963  choicefi  45977  supxrgere  46109  supxrgelem  46113  supxrge  46114  suplesup  46115  infxr  46142  infleinflem2  46146  rexabslelem  46192  fmul01lt1  46362  limcleqr  46418  limclner  46425  dvnprodlem1  46720  volioc  46746  stoweidlem60  46834  wallispilem3  46841  fourierdlem12  46893  fourierdlem41  46922  fourierdlem42  46923  fourierdlem48  46928  fourierdlem49  46929  fourierdlem54  46934  fourierdlem68  46948  fourierdlem73  46953  fourierdlem74  46954  fourierdlem75  46955  fourierdlem83  46963  elaa2  47008  etransclem24  47032  etransclem32  47040  ioorrnopnlem  47078  issalnnd  47119  sge0xaddlem2  47208  sge0seq  47220  meaiininc2  47262  hoicvr  47322  ovnsubaddlem2  47345  hoidmvval0  47361  hoidmvlelem3  47371  hspmbllem2  47401  vonioo  47456  vonicc  47459  smfinflem  47591  fsupdm  47616  finfdm  47620  fmtnoprmfac2lem1  48378  fmtnofac1  48382  lincresunit3lem3  49313  suppdm  49349  inlinecirc02p  49626