Theorem 3ad2antl1 1187

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

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

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 1089

This theorem is referenced by:  simpl1  1193  simpl1l  1226  simpl1r  1227  simpl11  1250  simpl12  1251  simpl13  1252  smocdmdom  8308  omeulem1  8517  f1oen4g  8911  f1dom4g  8912  dif1ennnALT  9187  ordiso2  9430  infpssrlem4  10228  fin1a2lem9  10330  gchpwdom  10593  tskwun  10707  gruxp  10730  infregelb  12140  fzo1fzo0n0  13670  fsuppmapnn0fiub  13953  pfxsuffeqwrdeq  14660  fprodle  15961  muldvds2  16250  dvds2add  16259  dvds2sub  16260  dvdstr  16263  lcmfledvds  16601  mndvcl  18765  mhmvlin  18769  mulgnnsubcl  19062  mulgpropd  19092  gexdvdsi  19558  ringidss  20258  reslmhm2  21048  obs2ss  21709  lsslindf  21810  issubassa  21847  madurid  22609  restntr  23147  cnpnei  23229  upxp  23588  qtopss  23680  opnfbas  23807  fbasrn  23849  trfg  23856  ufilmax  23872  ustuqtop1  24206  prdsxmetlem  24333  nmoix  24694  nmoi2  24695  iimulcl  24904  mbfimaopn2  25624  lgsval4lem  27271  nodenselem8  27655  f1otrg  28939  brbtwn2  28974  colinearalg  28979  axsegconlem1  28986  0vtxrusgr  29646  clwwlkccatlem  30059  clwwlkccat  30060  clwwisshclwws  30085  clwwlkfo  30120  numclwwlk1lem2fo  30428  lnosub  30830  pjspansn  31648  eulerpartlemb  34512  cnpconn  35412  mclspps  35766  curf  37919  mblfinlem2  37979  mblfinlem3  37980  mettrifi  38078  ghomdiv  38213  grpokerinj  38214  rngohomco  38295  crngohomfo  38327  keridl  38353  cvrcon3b  39723  mzpsubst  43180  lzunuz  43200  diophrex  43207  rmxycomplete  43345  jm2.26  43430  lnmepi  43513  lmhmlnmsplit  43515  nadd2rabex  43814  nadd1rabtr  43816  nadd1rabex  43818  ntrclsiso  44494  ntrclskb  44496  ntrclsk3  44497  uzwo4  45484  wessf1ornlem  45615  choicefi  45629  supxrgere  45763  supxrgelem  45767  supxrge  45768  suplesup  45769  infxr  45796  infleinflem2  45800  rexabslelem  45846  fmul01lt1  46016  limcleqr  46072  limclner  46079  dvnprodlem1  46374  volioc  46400  stoweidlem60  46488  wallispilem3  46495  fourierdlem12  46547  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem54  46588  fourierdlem68  46602  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem83  46617  elaa2  46662  etransclem24  46686  etransclem32  46694  ioorrnopnlem  46732  issalnnd  46773  sge0xaddlem2  46862  sge0seq  46874  meaiininc2  46916  hoicvr  46976  ovnsubaddlem2  46999  hoidmvval0  47015  hoidmvlelem3  47025  hspmbllem2  47055  vonioo  47110  vonicc  47113  smfinflem  47245  fsupdm  47270  finfdm  47274  fmtnoprmfac2lem1  48029  fmtnofac1  48033  lincresunit3lem3  48950  suppdm  48986  inlinecirc02p  49263