Theorem 3ad2antl1 1187

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 716	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1169	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  1193  simpl1l  1226  simpl1r  1227  simpl11  1250  simpl12  1251  simpl13  1252  smocdmdom  8310  omeulem1  8519  f1oen4g  8913  f1dom4g  8914  dif1ennnALT  9189  ordiso2  9432  infpssrlem4  10228  fin1a2lem9  10330  gchpwdom  10593  tskwun  10707  gruxp  10730  infregelb  12138  fzo1fzo0n0  13643  fsuppmapnn0fiub  13926  pfxsuffeqwrdeq  14633  fprodle  15931  muldvds2  16220  dvds2add  16229  dvds2sub  16230  dvdstr  16233  lcmfledvds  16571  mndvcl  18734  mhmvlin  18738  mulgnnsubcl  19028  mulgpropd  19058  gexdvdsi  19524  ringidss  20224  reslmhm2  21017  obs2ss  21696  lsslindf  21797  issubassa  21834  madurid  22600  restntr  23138  cnpnei  23220  upxp  23579  qtopss  23671  opnfbas  23798  fbasrn  23840  trfg  23847  ufilmax  23863  ustuqtop1  24197  prdsxmetlem  24324  nmoix  24685  nmoi2  24686  iimulcl  24901  mbfimaopn2  25626  lgsval4lem  27287  nodenselem8  27671  f1otrg  28955  brbtwn2  28990  colinearalg  28995  axsegconlem1  29002  0vtxrusgr  29663  clwwlkccatlem  30076  clwwlkccat  30077  clwwisshclwws  30102  clwwlkfo  30137  numclwwlk1lem2fo  30445  lnosub  30847  pjspansn  31665  eulerpartlemb  34546  cnpconn  35446  mclspps  35800  curf  37849  mblfinlem2  37909  mblfinlem3  37910  mettrifi  38008  ghomdiv  38143  grpokerinj  38144  rngohomco  38225  crngohomfo  38257  keridl  38283  cvrcon3b  39653  mzpsubst  43105  lzunuz  43125  diophrex  43132  rmxycomplete  43274  jm2.26  43359  lnmepi  43442  lmhmlnmsplit  43444  nadd2rabex  43743  nadd1rabtr  43745  nadd1rabex  43747  ntrclsiso  44423  ntrclskb  44425  ntrclsk3  44426  uzwo4  45413  wessf1ornlem  45544  choicefi  45558  supxrgere  45692  supxrgelem  45696  supxrge  45697  suplesup  45698  infxr  45725  infleinflem2  45729  rexabslelem  45776  fmul01lt1  45946  limcleqr  46002  limclner  46009  dvnprodlem1  46304  volioc  46330  stoweidlem60  46418  wallispilem3  46425  fourierdlem12  46477  fourierdlem41  46506  fourierdlem42  46507  fourierdlem48  46512  fourierdlem49  46513  fourierdlem54  46518  fourierdlem68  46532  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem83  46547  elaa2  46592  etransclem24  46616  etransclem32  46624  ioorrnopnlem  46662  issalnnd  46703  sge0xaddlem2  46792  sge0seq  46804  meaiininc2  46846  hoicvr  46906  ovnsubaddlem2  46929  hoidmvval0  46945  hoidmvlelem3  46955  hspmbllem2  46985  vonioo  47040  vonicc  47043  smfinflem  47175  fsupdm  47200  finfdm  47204  fmtnoprmfac2lem1  47926  fmtnofac1  47930  lincresunit3lem3  48834  suppdm  48870  inlinecirc02p  49147