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  8288  omeulem1  8497  f1oen4g  8887  f1dom4g  8888  dif1ennnALT  9161  ordiso2  9401  infpssrlem4  10197  fin1a2lem9  10299  gchpwdom  10561  tskwun  10675  gruxp  10698  infregelb  12106  fzo1fzo0n0  13615  fsuppmapnn0fiub  13898  pfxsuffeqwrdeq  14605  fprodle  15903  muldvds2  16192  dvds2add  16201  dvds2sub  16202  dvdstr  16205  lcmfledvds  16543  mndvcl  18705  mhmvlin  18709  mulgnnsubcl  18999  mulgpropd  19029  gexdvdsi  19495  ringidss  20195  reslmhm2  20987  obs2ss  21666  lsslindf  21767  issubassa  21804  madurid  22559  restntr  23097  cnpnei  23179  upxp  23538  qtopss  23630  opnfbas  23757  fbasrn  23799  trfg  23806  ufilmax  23822  ustuqtop1  24156  prdsxmetlem  24283  nmoix  24644  nmoi2  24645  iimulcl  24860  mbfimaopn2  25585  lgsval4lem  27246  nodenselem8  27630  f1otrg  28849  brbtwn2  28883  colinearalg  28888  axsegconlem1  28895  0vtxrusgr  29556  clwwlkccatlem  29969  clwwlkccat  29970  clwwisshclwws  29995  clwwlkfo  30030  numclwwlk1lem2fo  30338  lnosub  30739  pjspansn  31557  eulerpartlemb  34381  cnpconn  35274  mclspps  35628  curf  37648  mblfinlem2  37708  mblfinlem3  37709  mettrifi  37807  ghomdiv  37942  grpokerinj  37943  rngohomco  38024  crngohomfo  38056  keridl  38082  cvrcon3b  39386  mzpsubst  42851  lzunuz  42871  diophrex  42878  rmxycomplete  43020  jm2.26  43105  lnmepi  43188  lmhmlnmsplit  43190  nadd2rabex  43489  nadd1rabtr  43491  nadd1rabex  43493  ntrclsiso  44170  ntrclskb  44172  ntrclsk3  44173  uzwo4  45160  wessf1ornlem  45292  choicefi  45307  supxrgere  45442  supxrgelem  45446  supxrge  45447  suplesup  45448  infxr  45475  infleinflem2  45479  rexabslelem  45526  fmul01lt1  45696  limcleqr  45752  limclner  45759  dvnprodlem1  46054  volioc  46080  stoweidlem60  46168  wallispilem3  46175  fourierdlem12  46227  fourierdlem41  46256  fourierdlem42  46257  fourierdlem48  46262  fourierdlem49  46263  fourierdlem54  46268  fourierdlem68  46282  fourierdlem73  46287  fourierdlem74  46288  fourierdlem75  46289  fourierdlem83  46297  elaa2  46342  etransclem24  46366  etransclem32  46374  ioorrnopnlem  46412  issalnnd  46453  sge0xaddlem2  46542  sge0seq  46554  meaiininc2  46596  hoicvr  46656  ovnsubaddlem2  46679  hoidmvval0  46695  hoidmvlelem3  46705  hspmbllem2  46735  vonioo  46790  vonicc  46793  smfinflem  46925  fsupdm  46950  finfdm  46954  fmtnoprmfac2lem1  47676  fmtnofac1  47680  lincresunit3lem3  48585  suppdm  48621  inlinecirc02p  48898