MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ad2antl1 Structured version   Visualization version   GIF version

Theorem 3ad2antl1 1185
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
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantlr 713 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1167 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  simpl1  1191  simpl1l  1224  simpl1r  1225  simpl11  1248  simpl12  1249  simpl13  1250  smocdmdom  8314  omeulem1  8529  f1oen4g  8904  f1dom4g  8905  dif1ennnALT  9221  ordiso2  9451  infpssrlem4  10242  fin1a2lem9  10344  gchpwdom  10606  tskwun  10720  gruxp  10743  infregelb  12139  fzo1fzo0n0  13623  fsuppmapnn0fiub  13896  pfxsuffeqwrdeq  14586  fprodle  15879  muldvds2  16164  dvds2add  16172  dvds2sub  16173  dvdstr  16176  lcmfledvds  16508  mulgnnsubcl  18888  mulgpropd  18918  gexdvdsi  19365  ringidss  19998  reslmhm2  20514  obs2ss  21135  lsslindf  21236  issubassa  21272  mndvcl  21740  mhmvlin  21746  madurid  21993  restntr  22533  cnpnei  22615  upxp  22974  qtopss  23066  opnfbas  23193  fbasrn  23235  trfg  23242  ufilmax  23258  ustuqtop1  23593  prdsxmetlem  23721  nmoix  24093  nmoi2  24094  iimulcl  24300  mbfimaopn2  25021  lgsval4lem  26656  nodenselem8  27039  f1otrg  27813  brbtwn2  27854  colinearalg  27859  axsegconlem1  27866  0vtxrusgr  28525  clwwlkccatlem  28933  clwwlkccat  28934  clwwisshclwws  28959  clwwlkfo  28994  numclwwlk1lem2fo  29302  lnosub  29701  pjspansn  30519  eulerpartlemb  32968  cnpconn  33824  mclspps  34178  curf  36056  mblfinlem2  36116  mblfinlem3  36117  mettrifi  36216  ghomdiv  36351  grpokerinj  36352  rngohomco  36433  crngohomfo  36465  keridl  36491  cvrcon3b  37739  factwoffsmonot  40615  mzpsubst  41057  lzunuz  41077  diophrex  41084  rmxycomplete  41227  jm2.26  41312  lnmepi  41398  lmhmlnmsplit  41400  ntrclsiso  42329  ntrclskb  42331  ntrclsk3  42332  uzwo4  43251  wessf1ornlem  43393  choicefi  43411  supxrgere  43557  supxrgelem  43561  supxrge  43562  suplesup  43563  infxr  43591  infleinflem2  43595  rexabslelem  43643  fmul01lt1  43817  limcleqr  43875  limclner  43882  dvnprodlem1  44177  volioc  44203  stoweidlem60  44291  wallispilem3  44298  fourierdlem12  44350  fourierdlem41  44379  fourierdlem42  44380  fourierdlem48  44385  fourierdlem49  44386  fourierdlem54  44391  fourierdlem68  44405  fourierdlem73  44410  fourierdlem74  44411  fourierdlem75  44412  fourierdlem83  44420  elaa2  44465  etransclem24  44489  etransclem32  44497  ioorrnopnlem  44535  issalnnd  44576  sge0xaddlem2  44665  sge0seq  44677  meaiininc2  44719  hoicvr  44779  ovnsubaddlem2  44802  hoidmvval0  44818  hoidmvlelem3  44828  hspmbllem2  44858  vonioo  44913  vonicc  44916  smfinflem  45048  fsupdm  45073  finfdm  45077  fmtnoprmfac2lem1  45748  fmtnofac1  45752  lincresunit3lem3  46545  suppdm  46581  inlinecirc02p  46863
  Copyright terms: Public domain W3C validator