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  8340  omeulem1  8549  f1oen4g  8939  f1dom4g  8940  dif1ennnALT  9229  ordiso2  9475  infpssrlem4  10266  fin1a2lem9  10368  gchpwdom  10630  tskwun  10744  gruxp  10767  infregelb  12174  fzo1fzo0n0  13683  fsuppmapnn0fiub  13963  pfxsuffeqwrdeq  14670  fprodle  15969  muldvds2  16258  dvds2add  16267  dvds2sub  16268  dvdstr  16271  lcmfledvds  16609  mndvcl  18731  mhmvlin  18735  mulgnnsubcl  19025  mulgpropd  19055  gexdvdsi  19520  ringidss  20193  reslmhm2  20967  obs2ss  21645  lsslindf  21746  issubassa  21783  madurid  22538  restntr  23076  cnpnei  23158  upxp  23517  qtopss  23609  opnfbas  23736  fbasrn  23778  trfg  23785  ufilmax  23801  ustuqtop1  24136  prdsxmetlem  24263  nmoix  24624  nmoi2  24625  iimulcl  24840  mbfimaopn2  25565  lgsval4lem  27226  nodenselem8  27610  f1otrg  28805  brbtwn2  28839  colinearalg  28844  axsegconlem1  28851  0vtxrusgr  29512  clwwlkccatlem  29925  clwwlkccat  29926  clwwisshclwws  29951  clwwlkfo  29986  numclwwlk1lem2fo  30294  lnosub  30695  pjspansn  31513  eulerpartlemb  34366  cnpconn  35224  mclspps  35578  curf  37599  mblfinlem2  37659  mblfinlem3  37660  mettrifi  37758  ghomdiv  37893  grpokerinj  37894  rngohomco  37975  crngohomfo  38007  keridl  38033  cvrcon3b  39277  mzpsubst  42743  lzunuz  42763  diophrex  42770  rmxycomplete  42913  jm2.26  42998  lnmepi  43081  lmhmlnmsplit  43083  nadd2rabex  43382  nadd1rabtr  43384  nadd1rabex  43386  ntrclsiso  44063  ntrclskb  44065  ntrclsk3  44066  uzwo4  45054  wessf1ornlem  45186  choicefi  45201  supxrgere  45336  supxrgelem  45340  supxrge  45341  suplesup  45342  infxr  45370  infleinflem2  45374  rexabslelem  45421  fmul01lt1  45591  limcleqr  45649  limclner  45656  dvnprodlem1  45951  volioc  45977  stoweidlem60  46065  wallispilem3  46072  fourierdlem12  46124  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem54  46165  fourierdlem68  46179  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem83  46194  elaa2  46239  etransclem24  46263  etransclem32  46271  ioorrnopnlem  46309  issalnnd  46350  sge0xaddlem2  46439  sge0seq  46451  meaiininc2  46493  hoicvr  46553  ovnsubaddlem2  46576  hoidmvval0  46592  hoidmvlelem3  46602  hspmbllem2  46632  vonioo  46687  vonicc  46690  smfinflem  46822  fsupdm  46847  finfdm  46851  fmtnoprmfac2lem1  47571  fmtnofac1  47575  lincresunit3lem3  48467  suppdm  48503  inlinecirc02p  48780