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  8314  omeulem1  8523  f1oen4g  8913  f1dom4g  8914  dif1ennnALT  9198  ordiso2  9444  infpssrlem4  10235  fin1a2lem9  10337  gchpwdom  10599  tskwun  10713  gruxp  10736  infregelb  12143  fzo1fzo0n0  13652  fsuppmapnn0fiub  13932  pfxsuffeqwrdeq  14639  fprodle  15938  muldvds2  16227  dvds2add  16236  dvds2sub  16237  dvdstr  16240  lcmfledvds  16578  mndvcl  18706  mhmvlin  18710  mulgnnsubcl  19000  mulgpropd  19030  gexdvdsi  19497  ringidss  20197  reslmhm2  20992  obs2ss  21671  lsslindf  21772  issubassa  21809  madurid  22564  restntr  23102  cnpnei  23184  upxp  23543  qtopss  23635  opnfbas  23762  fbasrn  23804  trfg  23811  ufilmax  23827  ustuqtop1  24162  prdsxmetlem  24289  nmoix  24650  nmoi2  24651  iimulcl  24866  mbfimaopn2  25591  lgsval4lem  27252  nodenselem8  27636  f1otrg  28851  brbtwn2  28885  colinearalg  28890  axsegconlem1  28897  0vtxrusgr  29558  clwwlkccatlem  29968  clwwlkccat  29969  clwwisshclwws  29994  clwwlkfo  30029  numclwwlk1lem2fo  30337  lnosub  30738  pjspansn  31556  eulerpartlemb  34352  cnpconn  35210  mclspps  35564  curf  37585  mblfinlem2  37645  mblfinlem3  37646  mettrifi  37744  ghomdiv  37879  grpokerinj  37880  rngohomco  37961  crngohomfo  37993  keridl  38019  cvrcon3b  39263  mzpsubst  42729  lzunuz  42749  diophrex  42756  rmxycomplete  42899  jm2.26  42984  lnmepi  43067  lmhmlnmsplit  43069  nadd2rabex  43368  nadd1rabtr  43370  nadd1rabex  43372  ntrclsiso  44049  ntrclskb  44051  ntrclsk3  44052  uzwo4  45040  wessf1ornlem  45172  choicefi  45187  supxrgere  45322  supxrgelem  45326  supxrge  45327  suplesup  45328  infxr  45356  infleinflem2  45360  rexabslelem  45407  fmul01lt1  45577  limcleqr  45635  limclner  45642  dvnprodlem1  45937  volioc  45963  stoweidlem60  46051  wallispilem3  46058  fourierdlem12  46110  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem54  46151  fourierdlem68  46165  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem83  46180  elaa2  46225  etransclem24  46249  etransclem32  46257  ioorrnopnlem  46295  issalnnd  46336  sge0xaddlem2  46425  sge0seq  46437  meaiininc2  46479  hoicvr  46539  ovnsubaddlem2  46562  hoidmvval0  46578  hoidmvlelem3  46588  hspmbllem2  46618  vonioo  46673  vonicc  46676  smfinflem  46808  fsupdm  46833  finfdm  46837  fmtnoprmfac2lem1  47560  fmtnofac1  47564  lincresunit3lem3  48456  suppdm  48492  inlinecirc02p  48769