Theorem 3ad2antl1 1186

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 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1168	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  1192  simpl1l  1225  simpl1r  1226  simpl11  1249  simpl12  1250  simpl13  1251  smocdmdom  8408  omeulem1  8620  f1oen4g  9005  f1dom4g  9006  dif1ennnALT  9311  ordiso2  9555  infpssrlem4  10346  fin1a2lem9  10448  gchpwdom  10710  tskwun  10824  gruxp  10847  infregelb  12252  fzo1fzo0n0  13754  fsuppmapnn0fiub  14032  pfxsuffeqwrdeq  14736  fprodle  16032  muldvds2  16319  dvds2add  16327  dvds2sub  16328  dvdstr  16331  lcmfledvds  16669  mndvcl  18810  mhmvlin  18814  mulgnnsubcl  19104  mulgpropd  19134  gexdvdsi  19601  ringidss  20274  reslmhm2  21052  obs2ss  21749  lsslindf  21850  issubassa  21887  madurid  22650  restntr  23190  cnpnei  23272  upxp  23631  qtopss  23723  opnfbas  23850  fbasrn  23892  trfg  23899  ufilmax  23915  ustuqtop1  24250  prdsxmetlem  24378  nmoix  24750  nmoi2  24751  iimulcl  24966  mbfimaopn2  25692  lgsval4lem  27352  nodenselem8  27736  f1otrg  28879  brbtwn2  28920  colinearalg  28925  axsegconlem1  28932  0vtxrusgr  29595  clwwlkccatlem  30008  clwwlkccat  30009  clwwisshclwws  30034  clwwlkfo  30069  numclwwlk1lem2fo  30377  lnosub  30778  pjspansn  31596  eulerpartlemb  34370  cnpconn  35235  mclspps  35589  curf  37605  mblfinlem2  37665  mblfinlem3  37666  mettrifi  37764  ghomdiv  37899  grpokerinj  37900  rngohomco  37981  crngohomfo  38013  keridl  38039  cvrcon3b  39278  factwoffsmonot  42243  mzpsubst  42759  lzunuz  42779  diophrex  42786  rmxycomplete  42929  jm2.26  43014  lnmepi  43097  lmhmlnmsplit  43099  nadd2rabex  43399  nadd1rabtr  43401  nadd1rabex  43403  ntrclsiso  44080  ntrclskb  44082  ntrclsk3  44083  uzwo4  45058  wessf1ornlem  45190  choicefi  45205  supxrgere  45344  supxrgelem  45348  supxrge  45349  suplesup  45350  infxr  45378  infleinflem2  45382  rexabslelem  45429  fmul01lt1  45601  limcleqr  45659  limclner  45666  dvnprodlem1  45961  volioc  45987  stoweidlem60  46075  wallispilem3  46082  fourierdlem12  46134  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem54  46175  fourierdlem68  46189  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem83  46204  elaa2  46249  etransclem24  46273  etransclem32  46281  ioorrnopnlem  46319  issalnnd  46360  sge0xaddlem2  46449  sge0seq  46461  meaiininc2  46503  hoicvr  46563  ovnsubaddlem2  46586  hoidmvval0  46602  hoidmvlelem3  46612  hspmbllem2  46642  vonioo  46697  vonicc  46700  smfinflem  46832  fsupdm  46857  finfdm  46861  fmtnoprmfac2lem1  47553  fmtnofac1  47557  lincresunit3lem3  48391  suppdm  48427  inlinecirc02p  48708