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  8337  omeulem1  8546  f1oen4g  8936  f1dom4g  8937  dif1ennnALT  9222  ordiso2  9468  infpssrlem4  10259  fin1a2lem9  10361  gchpwdom  10623  tskwun  10737  gruxp  10760  infregelb  12167  fzo1fzo0n0  13676  fsuppmapnn0fiub  13956  pfxsuffeqwrdeq  14663  fprodle  15962  muldvds2  16251  dvds2add  16260  dvds2sub  16261  dvdstr  16264  lcmfledvds  16602  mndvcl  18724  mhmvlin  18728  mulgnnsubcl  19018  mulgpropd  19048  gexdvdsi  19513  ringidss  20186  reslmhm2  20960  obs2ss  21638  lsslindf  21739  issubassa  21776  madurid  22531  restntr  23069  cnpnei  23151  upxp  23510  qtopss  23602  opnfbas  23729  fbasrn  23771  trfg  23778  ufilmax  23794  ustuqtop1  24129  prdsxmetlem  24256  nmoix  24617  nmoi2  24618  iimulcl  24833  mbfimaopn2  25558  lgsval4lem  27219  nodenselem8  27603  f1otrg  28798  brbtwn2  28832  colinearalg  28837  axsegconlem1  28844  0vtxrusgr  29505  clwwlkccatlem  29918  clwwlkccat  29919  clwwisshclwws  29944  clwwlkfo  29979  numclwwlk1lem2fo  30287  lnosub  30688  pjspansn  31506  eulerpartlemb  34359  cnpconn  35217  mclspps  35571  curf  37592  mblfinlem2  37652  mblfinlem3  37653  mettrifi  37751  ghomdiv  37886  grpokerinj  37887  rngohomco  37968  crngohomfo  38000  keridl  38026  cvrcon3b  39270  mzpsubst  42736  lzunuz  42756  diophrex  42763  rmxycomplete  42906  jm2.26  42991  lnmepi  43074  lmhmlnmsplit  43076  nadd2rabex  43375  nadd1rabtr  43377  nadd1rabex  43379  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  uzwo4  45047  wessf1ornlem  45179  choicefi  45194  supxrgere  45329  supxrgelem  45333  supxrge  45334  suplesup  45335  infxr  45363  infleinflem2  45367  rexabslelem  45414  fmul01lt1  45584  limcleqr  45642  limclner  45649  dvnprodlem1  45944  volioc  45970  stoweidlem60  46058  wallispilem3  46065  fourierdlem12  46117  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem54  46158  fourierdlem68  46172  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem83  46187  elaa2  46232  etransclem24  46256  etransclem32  46264  ioorrnopnlem  46302  issalnnd  46343  sge0xaddlem2  46432  sge0seq  46444  meaiininc2  46486  hoicvr  46546  ovnsubaddlem2  46569  hoidmvval0  46585  hoidmvlelem3  46595  hspmbllem2  46625  vonioo  46680  vonicc  46683  smfinflem  46815  fsupdm  46840  finfdm  46844  fmtnoprmfac2lem1  47567  fmtnofac1  47571  lincresunit3lem3  48463  suppdm  48499  inlinecirc02p  48776