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  8300  omeulem1  8509  f1oen4g  8901  f1dom4g  8902  dif1ennnALT  9177  ordiso2  9420  infpssrlem4  10216  fin1a2lem9  10318  gchpwdom  10581  tskwun  10695  gruxp  10718  infregelb  12126  fzo1fzo0n0  13631  fsuppmapnn0fiub  13914  pfxsuffeqwrdeq  14621  fprodle  15919  muldvds2  16208  dvds2add  16217  dvds2sub  16218  dvdstr  16221  lcmfledvds  16559  mndvcl  18722  mhmvlin  18726  mulgnnsubcl  19016  mulgpropd  19046  gexdvdsi  19512  ringidss  20212  reslmhm2  21005  obs2ss  21684  lsslindf  21785  issubassa  21822  madurid  22588  restntr  23126  cnpnei  23208  upxp  23567  qtopss  23659  opnfbas  23786  fbasrn  23828  trfg  23835  ufilmax  23851  ustuqtop1  24185  prdsxmetlem  24312  nmoix  24673  nmoi2  24674  iimulcl  24889  mbfimaopn2  25614  lgsval4lem  27275  nodenselem8  27659  f1otrg  28943  brbtwn2  28978  colinearalg  28983  axsegconlem1  28990  0vtxrusgr  29651  clwwlkccatlem  30064  clwwlkccat  30065  clwwisshclwws  30090  clwwlkfo  30125  numclwwlk1lem2fo  30433  lnosub  30834  pjspansn  31652  eulerpartlemb  34525  cnpconn  35424  mclspps  35778  curf  37799  mblfinlem2  37859  mblfinlem3  37860  mettrifi  37958  ghomdiv  38093  grpokerinj  38094  rngohomco  38175  crngohomfo  38207  keridl  38233  cvrcon3b  39547  mzpsubst  43000  lzunuz  43020  diophrex  43027  rmxycomplete  43169  jm2.26  43254  lnmepi  43337  lmhmlnmsplit  43339  nadd2rabex  43638  nadd1rabtr  43640  nadd1rabex  43642  ntrclsiso  44318  ntrclskb  44320  ntrclsk3  44321  uzwo4  45308  wessf1ornlem  45439  choicefi  45454  supxrgere  45588  supxrgelem  45592  supxrge  45593  suplesup  45594  infxr  45621  infleinflem2  45625  rexabslelem  45672  fmul01lt1  45842  limcleqr  45898  limclner  45905  dvnprodlem1  46200  volioc  46226  stoweidlem60  46314  wallispilem3  46321  fourierdlem12  46373  fourierdlem41  46402  fourierdlem42  46403  fourierdlem48  46408  fourierdlem49  46409  fourierdlem54  46414  fourierdlem68  46428  fourierdlem73  46433  fourierdlem74  46434  fourierdlem75  46435  fourierdlem83  46443  elaa2  46488  etransclem24  46512  etransclem32  46520  ioorrnopnlem  46558  issalnnd  46599  sge0xaddlem2  46688  sge0seq  46700  meaiininc2  46742  hoicvr  46802  ovnsubaddlem2  46825  hoidmvval0  46841  hoidmvlelem3  46851  hspmbllem2  46881  vonioo  46936  vonicc  46939  smfinflem  47071  fsupdm  47096  finfdm  47100  fmtnoprmfac2lem1  47822  fmtnofac1  47826  lincresunit3lem3  48730  suppdm  48766  inlinecirc02p  49043