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 1086

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 1088

This theorem is referenced by:  simpl1  1192  simpl1l  1225  simpl1r  1226  simpl11  1249  simpl12  1250  simpl13  1251  smocdmdom  8291  omeulem1  8500  f1oen4g  8890  f1dom4g  8891  dif1ennnALT  9166  ordiso2  9407  infpssrlem4  10200  fin1a2lem9  10302  gchpwdom  10564  tskwun  10678  gruxp  10701  infregelb  12109  fzo1fzo0n0  13618  fsuppmapnn0fiub  13898  pfxsuffeqwrdeq  14604  fprodle  15903  muldvds2  16192  dvds2add  16201  dvds2sub  16202  dvdstr  16205  lcmfledvds  16543  mndvcl  18671  mhmvlin  18675  mulgnnsubcl  18965  mulgpropd  18995  gexdvdsi  19462  ringidss  20162  reslmhm2  20957  obs2ss  21636  lsslindf  21737  issubassa  21774  madurid  22529  restntr  23067  cnpnei  23149  upxp  23508  qtopss  23600  opnfbas  23727  fbasrn  23769  trfg  23776  ufilmax  23792  ustuqtop1  24127  prdsxmetlem  24254  nmoix  24615  nmoi2  24616  iimulcl  24831  mbfimaopn2  25556  lgsval4lem  27217  nodenselem8  27601  f1otrg  28816  brbtwn2  28850  colinearalg  28855  axsegconlem1  28862  0vtxrusgr  29523  clwwlkccatlem  29933  clwwlkccat  29934  clwwisshclwws  29959  clwwlkfo  29994  numclwwlk1lem2fo  30302  lnosub  30703  pjspansn  31521  eulerpartlemb  34336  cnpconn  35207  mclspps  35561  curf  37582  mblfinlem2  37642  mblfinlem3  37643  mettrifi  37741  ghomdiv  37876  grpokerinj  37877  rngohomco  37958  crngohomfo  37990  keridl  38016  cvrcon3b  39260  mzpsubst  42725  lzunuz  42745  diophrex  42752  rmxycomplete  42894  jm2.26  42979  lnmepi  43062  lmhmlnmsplit  43064  nadd2rabex  43363  nadd1rabtr  43365  nadd1rabex  43367  ntrclsiso  44044  ntrclskb  44046  ntrclsk3  44047  uzwo4  45035  wessf1ornlem  45167  choicefi  45182  supxrgere  45317  supxrgelem  45321  supxrge  45322  suplesup  45323  infxr  45350  infleinflem2  45354  rexabslelem  45401  fmul01lt1  45571  limcleqr  45629  limclner  45636  dvnprodlem1  45931  volioc  45957  stoweidlem60  46045  wallispilem3  46052  fourierdlem12  46104  fourierdlem41  46133  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem54  46145  fourierdlem68  46159  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem83  46174  elaa2  46219  etransclem24  46243  etransclem32  46251  ioorrnopnlem  46289  issalnnd  46330  sge0xaddlem2  46419  sge0seq  46431  meaiininc2  46473  hoicvr  46533  ovnsubaddlem2  46556  hoidmvval0  46572  hoidmvlelem3  46582  hspmbllem2  46612  vonioo  46667  vonicc  46670  smfinflem  46802  fsupdm  46827  finfdm  46831  fmtnoprmfac2lem1  47554  fmtnofac1  47558  lincresunit3lem3  48463  suppdm  48499  inlinecirc02p  48776