Theorem 3ad2antl1 1185

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 1167	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  1191  simpl1l  1224  simpl1r  1225  simpl11  1248  simpl12  1249  simpl13  1250  smocdmdom  8424  omeulem1  8638  f1oen4g  9024  f1dom4g  9025  dif1ennnALT  9339  ordiso2  9584  infpssrlem4  10375  fin1a2lem9  10477  gchpwdom  10739  tskwun  10853  gruxp  10876  infregelb  12279  fzo1fzo0n0  13767  fsuppmapnn0fiub  14042  pfxsuffeqwrdeq  14746  fprodle  16044  muldvds2  16330  dvds2add  16338  dvds2sub  16339  dvdstr  16342  lcmfledvds  16679  mndvcl  18832  mhmvlin  18836  mulgnnsubcl  19126  mulgpropd  19156  gexdvdsi  19625  ringidss  20300  reslmhm2  21075  obs2ss  21772  lsslindf  21873  issubassa  21910  madurid  22671  restntr  23211  cnpnei  23293  upxp  23652  qtopss  23744  opnfbas  23871  fbasrn  23913  trfg  23920  ufilmax  23936  ustuqtop1  24271  prdsxmetlem  24399  nmoix  24771  nmoi2  24772  iimulcl  24985  mbfimaopn2  25711  lgsval4lem  27370  nodenselem8  27754  f1otrg  28897  brbtwn2  28938  colinearalg  28943  axsegconlem1  28950  0vtxrusgr  29613  clwwlkccatlem  30021  clwwlkccat  30022  clwwisshclwws  30047  clwwlkfo  30082  numclwwlk1lem2fo  30390  lnosub  30791  pjspansn  31609  eulerpartlemb  34333  cnpconn  35198  mclspps  35552  curf  37558  mblfinlem2  37618  mblfinlem3  37619  mettrifi  37717  ghomdiv  37852  grpokerinj  37853  rngohomco  37934  crngohomfo  37966  keridl  37992  cvrcon3b  39233  factwoffsmonot  42199  mzpsubst  42704  lzunuz  42724  diophrex  42731  rmxycomplete  42874  jm2.26  42959  lnmepi  43042  lmhmlnmsplit  43044  nadd2rabex  43348  nadd1rabtr  43350  nadd1rabex  43352  ntrclsiso  44029  ntrclskb  44031  ntrclsk3  44032  uzwo4  44955  wessf1ornlem  45092  choicefi  45107  supxrgere  45248  supxrgelem  45252  supxrge  45253  suplesup  45254  infxr  45282  infleinflem2  45286  rexabslelem  45333  fmul01lt1  45507  limcleqr  45565  limclner  45572  dvnprodlem1  45867  volioc  45893  stoweidlem60  45981  wallispilem3  45988  fourierdlem12  46040  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem54  46081  fourierdlem68  46095  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem83  46110  elaa2  46155  etransclem24  46179  etransclem32  46187  ioorrnopnlem  46225  issalnnd  46266  sge0xaddlem2  46355  sge0seq  46367  meaiininc2  46409  hoicvr  46469  ovnsubaddlem2  46492  hoidmvval0  46508  hoidmvlelem3  46518  hspmbllem2  46548  vonioo  46603  vonicc  46606  smfinflem  46738  fsupdm  46763  finfdm  46767  fmtnoprmfac2lem1  47440  fmtnofac1  47444  lincresunit3lem3  48203  suppdm  48239  inlinecirc02p  48521