Theorem 3ad2antl1 1180

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  simpl1  1186  simpl1l  1219  simpl1r  1220  simpl11  1243  simpl12  1244  simpl13  1245  smorndom  7997  omeulem1  8200  dif1en  8743  ordiso2  8971  infpssrlem4  9720  fin1a2lem9  9822  gchpwdom  10084  tskwun  10198  gruxp  10221  infregelb  11617  fzo1fzo0n0  13080  fsuppmapnn0fiub  13351  ccat2s1fvwOLD  13991  pfxsuffeqwrdeq  14052  fprodle  15342  muldvds2  15627  dvds2add  15635  dvds2sub  15636  dvdstr  15638  lcmfledvds  15968  mulgnnsubcl  18232  mulgpropd  18261  gexdvdsi  18700  ringidss  19319  reslmhm2  19817  issubassa  20090  obs2ss  20865  lsslindf  20966  mndvcl  20994  mhmvlin  21000  madurid  21245  restntr  21782  cnpnei  21864  upxp  22223  qtopss  22315  opnfbas  22442  fbasrn  22484  trfg  22491  ufilmax  22507  ustuqtop1  22842  prdsxmetlem  22970  nmoix  23330  nmoi2  23331  iimulcl  23533  mbfimaopn2  24250  lgsval4lem  25876  f1otrg  26649  brbtwn2  26683  colinearalg  26688  axsegconlem1  26695  0vtxrusgr  27351  clwwlkccatlem  27759  clwwlkccat  27760  clwwisshclwws  27785  clwwlkfo  27821  numclwwlk1lem2fo  28129  lnosub  28528  pjspansn  29346  eulerpartlemb  31619  cnpconn  32470  mclspps  32824  nodenselem8  33188  curf  34862  mblfinlem2  34922  mblfinlem3  34923  mettrifi  35024  ghomdiv  35162  grpokerinj  35163  rngohomco  35244  crngohomfo  35276  keridl  35302  cvrcon3b  36405  mzpsubst  39335  lzunuz  39355  diophrex  39362  rmxycomplete  39504  jm2.26  39589  lnmepi  39675  lmhmlnmsplit  39677  ntrclsiso  40407  ntrclskb  40409  ntrclsk3  40410  uzwo4  41305  wessf1ornlem  41434  choicefi  41452  supxrgere  41590  supxrgelem  41594  supxrge  41595  suplesup  41596  infxr  41624  infleinflem2  41628  rexabslelem  41681  fmul01lt1  41856  limcleqr  41914  limclner  41921  dvnprodlem1  42220  volioc  42246  stoweidlem60  42335  wallispilem3  42342  fourierdlem12  42394  fourierdlem41  42423  fourierdlem42  42424  fourierdlem48  42429  fourierdlem49  42430  fourierdlem54  42435  fourierdlem68  42449  fourierdlem73  42454  fourierdlem74  42455  fourierdlem75  42456  fourierdlem83  42464  elaa2  42509  etransclem24  42533  etransclem32  42541  ioorrnopnlem  42579  issalnnd  42618  sge0xaddlem2  42706  sge0seq  42718  meaiininc2  42760  hoicvr  42820  ovnsubaddlem2  42843  hoidmvval0  42859  hoidmvlelem3  42869  hspmbllem2  42899  vonioo  42954  vonicc  42957  smfinflem  43081  fmtnoprmfac2lem1  43718  fmtnofac1  43722  lincresunit3lem3  44519  suppdm  44555  inlinecirc02p  44764