Theorem 3ad2antl1 1182

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 714	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1164	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpl1  1188  simpl1l  1221  simpl1r  1222  simpl11  1245  simpl12  1246  simpl13  1247  smorndom  8020  omeulem1  8223  dif1enOLD  8792  ordiso2  9017  infpssrlem4  9771  fin1a2lem9  9873  gchpwdom  10135  tskwun  10249  gruxp  10272  infregelb  11666  fzo1fzo0n0  13142  fsuppmapnn0fiub  13413  ccat2s1fvwOLD  14051  pfxsuffeqwrdeq  14112  fprodle  15403  muldvds2  15688  dvds2add  15696  dvds2sub  15697  dvdstr  15700  lcmfledvds  16033  mulgnnsubcl  18312  mulgpropd  18341  gexdvdsi  18780  ringidss  19403  reslmhm2  19898  obs2ss  20499  lsslindf  20600  issubassa  20636  mndvcl  21098  mhmvlin  21104  madurid  21349  restntr  21887  cnpnei  21969  upxp  22328  qtopss  22420  opnfbas  22547  fbasrn  22589  trfg  22596  ufilmax  22612  ustuqtop1  22947  prdsxmetlem  23075  nmoix  23436  nmoi2  23437  iimulcl  23643  mbfimaopn2  24362  lgsval4lem  25996  f1otrg  26769  brbtwn2  26803  colinearalg  26808  axsegconlem1  26815  0vtxrusgr  27471  clwwlkccatlem  27878  clwwlkccat  27879  clwwisshclwws  27904  clwwlkfo  27939  numclwwlk1lem2fo  28247  lnosub  28646  pjspansn  29464  eulerpartlemb  31858  cnpconn  32712  mclspps  33066  nodenselem8  33483  curf  35341  mblfinlem2  35401  mblfinlem3  35402  mettrifi  35501  ghomdiv  35636  grpokerinj  35637  rngohomco  35718  crngohomfo  35750  keridl  35776  cvrcon3b  36879  factwoffsmonot  39711  mzpsubst  40090  lzunuz  40110  diophrex  40117  rmxycomplete  40259  jm2.26  40344  lnmepi  40430  lmhmlnmsplit  40432  ntrclsiso  41171  ntrclskb  41173  ntrclsk3  41174  uzwo4  42088  wessf1ornlem  42209  choicefi  42227  supxrgere  42361  supxrgelem  42365  supxrge  42366  suplesup  42367  infxr  42395  infleinflem2  42399  rexabslelem  42449  fmul01lt1  42622  limcleqr  42680  limclner  42687  dvnprodlem1  42982  volioc  43008  stoweidlem60  43096  wallispilem3  43103  fourierdlem12  43155  fourierdlem41  43184  fourierdlem42  43185  fourierdlem48  43190  fourierdlem49  43191  fourierdlem54  43196  fourierdlem68  43210  fourierdlem73  43215  fourierdlem74  43216  fourierdlem75  43217  fourierdlem83  43225  elaa2  43270  etransclem24  43294  etransclem32  43302  ioorrnopnlem  43340  issalnnd  43379  sge0xaddlem2  43467  sge0seq  43479  meaiininc2  43521  hoicvr  43581  ovnsubaddlem2  43604  hoidmvval0  43620  hoidmvlelem3  43630  hspmbllem2  43660  vonioo  43715  vonicc  43718  smfinflem  43842  fmtnoprmfac2lem1  44479  fmtnofac1  44483  lincresunit3lem3  45276  suppdm  45312  inlinecirc02p  45594