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  8380  omeulem1  8592  f1oen4g  8977  f1dom4g  8978  dif1ennnALT  9281  ordiso2  9527  infpssrlem4  10318  fin1a2lem9  10420  gchpwdom  10682  tskwun  10796  gruxp  10819  infregelb  12224  fzo1fzo0n0  13729  fsuppmapnn0fiub  14007  pfxsuffeqwrdeq  14714  fprodle  16010  muldvds2  16299  dvds2add  16307  dvds2sub  16308  dvdstr  16311  lcmfledvds  16649  mndvcl  18773  mhmvlin  18777  mulgnnsubcl  19067  mulgpropd  19097  gexdvdsi  19562  ringidss  20235  reslmhm2  21009  obs2ss  21687  lsslindf  21788  issubassa  21825  madurid  22580  restntr  23118  cnpnei  23200  upxp  23559  qtopss  23651  opnfbas  23778  fbasrn  23820  trfg  23827  ufilmax  23843  ustuqtop1  24178  prdsxmetlem  24305  nmoix  24666  nmoi2  24667  iimulcl  24882  mbfimaopn2  25608  lgsval4lem  27269  nodenselem8  27653  f1otrg  28796  brbtwn2  28830  colinearalg  28835  axsegconlem1  28842  0vtxrusgr  29503  clwwlkccatlem  29916  clwwlkccat  29917  clwwisshclwws  29942  clwwlkfo  29977  numclwwlk1lem2fo  30285  lnosub  30686  pjspansn  31504  eulerpartlemb  34346  cnpconn  35198  mclspps  35552  curf  37568  mblfinlem2  37628  mblfinlem3  37629  mettrifi  37727  ghomdiv  37862  grpokerinj  37863  rngohomco  37944  crngohomfo  37976  keridl  38002  cvrcon3b  39241  factwoffsmonot  42201  mzpsubst  42718  lzunuz  42738  diophrex  42745  rmxycomplete  42888  jm2.26  42973  lnmepi  43056  lmhmlnmsplit  43058  nadd2rabex  43357  nadd1rabtr  43359  nadd1rabex  43361  ntrclsiso  44038  ntrclskb  44040  ntrclsk3  44041  uzwo4  45025  wessf1ornlem  45157  choicefi  45172  supxrgere  45308  supxrgelem  45312  supxrge  45313  suplesup  45314  infxr  45342  infleinflem2  45346  rexabslelem  45393  fmul01lt1  45563  limcleqr  45621  limclner  45628  dvnprodlem1  45923  volioc  45949  stoweidlem60  46037  wallispilem3  46044  fourierdlem12  46096  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem54  46137  fourierdlem68  46151  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem83  46166  elaa2  46211  etransclem24  46235  etransclem32  46243  ioorrnopnlem  46281  issalnnd  46322  sge0xaddlem2  46411  sge0seq  46423  meaiininc2  46465  hoicvr  46525  ovnsubaddlem2  46548  hoidmvval0  46564  hoidmvlelem3  46574  hspmbllem2  46604  vonioo  46659  vonicc  46662  smfinflem  46794  fsupdm  46819  finfdm  46823  fmtnoprmfac2lem1  47528  fmtnofac1  47532  lincresunit3lem3  48398  suppdm  48434  inlinecirc02p  48715