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  8302  omeulem1  8511  f1oen4g  8905  f1dom4g  8906  dif1ennnALT  9181  ordiso2  9424  infpssrlem4  10222  fin1a2lem9  10324  gchpwdom  10587  tskwun  10701  gruxp  10724  infregelb  12134  fzo1fzo0n0  13664  fsuppmapnn0fiub  13947  pfxsuffeqwrdeq  14654  fprodle  15955  muldvds2  16244  dvds2add  16253  dvds2sub  16254  dvdstr  16257  lcmfledvds  16595  mndvcl  18759  mhmvlin  18763  mulgnnsubcl  19056  mulgpropd  19086  gexdvdsi  19552  ringidss  20252  reslmhm2  21043  obs2ss  21722  lsslindf  21823  issubassa  21860  madurid  22622  restntr  23160  cnpnei  23242  upxp  23601  qtopss  23693  opnfbas  23820  fbasrn  23862  trfg  23869  ufilmax  23885  ustuqtop1  24219  prdsxmetlem  24346  nmoix  24707  nmoi2  24708  iimulcl  24917  mbfimaopn2  25637  lgsval4lem  27288  nodenselem8  27672  f1otrg  28956  brbtwn2  28991  colinearalg  28996  axsegconlem1  29003  0vtxrusgr  29664  clwwlkccatlem  30077  clwwlkccat  30078  clwwisshclwws  30103  clwwlkfo  30138  numclwwlk1lem2fo  30446  lnosub  30848  pjspansn  31666  eulerpartlemb  34531  cnpconn  35431  mclspps  35785  curf  37936  mblfinlem2  37996  mblfinlem3  37997  mettrifi  38095  ghomdiv  38230  grpokerinj  38231  rngohomco  38312  crngohomfo  38344  keridl  38370  cvrcon3b  39740  mzpsubst  43197  lzunuz  43217  diophrex  43224  rmxycomplete  43366  jm2.26  43451  lnmepi  43534  lmhmlnmsplit  43536  nadd2rabex  43835  nadd1rabtr  43837  nadd1rabex  43839  ntrclsiso  44515  ntrclskb  44517  ntrclsk3  44518  uzwo4  45505  wessf1ornlem  45636  choicefi  45650  supxrgere  45784  supxrgelem  45788  supxrge  45789  suplesup  45790  infxr  45817  infleinflem2  45821  rexabslelem  45867  fmul01lt1  46037  limcleqr  46093  limclner  46100  dvnprodlem1  46395  volioc  46421  stoweidlem60  46509  wallispilem3  46516  fourierdlem12  46568  fourierdlem41  46597  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem54  46609  fourierdlem68  46623  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem83  46638  elaa2  46683  etransclem24  46707  etransclem32  46715  ioorrnopnlem  46753  issalnnd  46794  sge0xaddlem2  46883  sge0seq  46895  meaiininc2  46937  hoicvr  46997  ovnsubaddlem2  47020  hoidmvval0  47036  hoidmvlelem3  47046  hspmbllem2  47076  vonioo  47131  vonicc  47134  smfinflem  47266  fsupdm  47291  finfdm  47295  fmtnoprmfac2lem1  48044  fmtnofac1  48048  lincresunit3lem3  48965  suppdm  49001  inlinecirc02p  49278