Theorem 3ad2antl1 1204

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl1  1210  simpl1l  1243  simpl1r  1244  simpl11  1267  simpl12  1268  simpl13  1269  smocdmdom  8376  omeulem1  8590  curf  8890  f1oen4g  8991  f1dom4g  8992  dif1ennnALT  9268  ordiso2  9509  infpssrlem4  10384  fin1a2lem9  10486  gchpwdom  10755  tskwun  10869  gruxp  10892  infregelb  12301  fzo1fzo0n0  13850  fsuppmapnn0fiub  14134  pfxsuffeqwrdeq  14847  fprodle  16163  muldvds2  16451  dvds2add  16460  dvds2sub  16461  dvdstr  16464  lcmfledvds  16807  mndvcl  18992  mhmvlin  18996  mulgnnsubcl  19296  mulgpropd  19326  gexdvdsi  19797  ringidss  20506  reslmhm2  21328  obs2ss  22035  lsslindf  22136  issubassa  22175  madurid  22959  restntr  23500  cnpnei  23582  upxp  23942  qtopss  24034  opnfbas  24161  fbasrn  24203  trfg  24210  ufilmax  24226  ustuqtop1  24560  prdsxmetlem  24687  nmoix  25048  nmoi2  25049  iimulcl  25258  mbfimaopn2  25978  lgsval4lem  27635  nodenselem8  28048  f1otrg  29448  brbtwn2  29483  colinearalg  29488  axsegconlem1  29495  0vtxrusgr  30158  clwwlkccatlem  30580  clwwlkccat  30581  clwwisshclwws  30606  clwwlkfo  30641  numclwwlk1lem2fo  30959  lnosub  31361  pjspansn  32179  eulerpartlemb  35000  cnpconn  35995  mclspps  36349  mblfinlem2  38576  mblfinlem3  38577  mettrifi  38691  ghomdiv  38826  grpokerinj  38827  rngohomco  38908  crngohomfo  38940  keridl  38966  cvrcon3b  40334  mzpsubst  43758  lzunuz  43778  diophrex  43785  rmxycomplete  43923  jm2.26  44008  lnmepi  44086  lmhmlnmsplit  44088  nadd2rabex  44387  nadd1rabtr  44389  nadd1rabex  44391  ntrclsiso  45066  ntrclskb  45068  ntrclsk3  45069  uzwo4  46069  wessf1ornlem  46199  choicefi  46213  supxrgere  46344  supxrgelem  46348  supxrge  46349  suplesup  46350  infxr  46377  infleinflem2  46381  rexabslelem  46427  fmul01lt1  46597  limcleqr  46653  limclner  46660  dvnprodlem1  46955  volioc  46981  stoweidlem60  47069  wallispilem3  47076  fourierdlem12  47128  fourierdlem41  47157  fourierdlem42  47158  fourierdlem48  47163  fourierdlem49  47164  fourierdlem54  47169  fourierdlem68  47183  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem83  47198  elaa2  47243  etransclem24  47267  etransclem32  47275  ioorrnopnlem  47313  issalnnd  47354  sge0xaddlem2  47443  sge0seq  47455  meaiininc2  47497  hoicvr  47557  ovnsubaddlem2  47580  hoidmvval0  47596  hoidmvlelem3  47606  hspmbllem2  47636  vonioo  47691  vonicc  47694  smfinflem  47826  fsupdm  47851  finfdm  47855  fmtnoprmfac2lem1  48650  fmtnofac1  48654  lincresunit3lem3  49585  suppdm  49621  inlinecirc02p  49898