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

Theorem 3ad2antl1 1179
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 711 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1161 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  simpl1  1185  simpl1l  1218  simpl1r  1219  simpl11  1242  simpl12  1243  simpl13  1244  smorndom  7999  omeulem1  8201  dif1en  8743  ordiso2  8971  infpssrlem4  9720  fin1a2lem9  9822  gchpwdom  10084  tskwun  10198  gruxp  10221  infregelb  11617  fzo1fzo0n0  13081  fsuppmapnn0fiub  13352  ccat2s1fvwOLD  13992  pfxsuffeqwrdeq  14053  fprodle  15342  muldvds2  15627  dvds2add  15635  dvds2sub  15636  dvdstr  15638  lcmfledvds  15968  mulgnnsubcl  18172  mulgpropd  18201  gexdvdsi  18630  ringidss  19249  reslmhm2  19747  issubassa  20019  obs2ss  20789  lsslindf  20890  mndvcl  20918  mhmvlin  20924  madurid  21169  restntr  21706  cnpnei  21788  upxp  22147  qtopss  22239  opnfbas  22366  fbasrn  22408  trfg  22415  ufilmax  22431  ustuqtop1  22765  prdsxmetlem  22893  nmoix  23253  nmoi2  23254  iimulcl  23456  mbfimaopn2  24173  lgsval4lem  25798  f1otrg  26571  brbtwn2  26605  colinearalg  26610  axsegconlem1  26617  0vtxrusgr  27273  clwwlkccatlem  27681  clwwlkccat  27682  clwwisshclwws  27707  clwwlkfo  27743  numclwwlk1lem2fo  28051  lnosub  28450  pjspansn  29268  eulerpartlemb  31512  cnpconn  32361  mclspps  32715  nodenselem8  33079  curf  34737  mblfinlem2  34797  mblfinlem3  34798  mettrifi  34900  ghomdiv  35038  grpokerinj  35039  rngohomco  35120  crngohomfo  35152  keridl  35178  cvrcon3b  36280  mzpsubst  39206  lzunuz  39226  diophrex  39233  rmxycomplete  39375  jm2.26  39460  lnmepi  39546  lmhmlnmsplit  39548  ntrclsiso  40278  ntrclskb  40280  ntrclsk3  40281  uzwo4  41176  wessf1ornlem  41306  choicefi  41324  supxrgere  41462  supxrgelem  41466  supxrge  41467  suplesup  41468  infxr  41496  infleinflem2  41500  rexabslelem  41553  fmul01lt1  41728  limcleqr  41786  limclner  41793  dvnprodlem1  42092  volioc  42118  stoweidlem60  42207  wallispilem3  42214  fourierdlem12  42266  fourierdlem41  42295  fourierdlem42  42296  fourierdlem48  42301  fourierdlem49  42302  fourierdlem54  42307  fourierdlem68  42321  fourierdlem73  42326  fourierdlem74  42327  fourierdlem75  42328  fourierdlem83  42336  elaa2  42381  etransclem24  42405  etransclem32  42413  ioorrnopnlem  42451  issalnnd  42490  sge0xaddlem2  42578  sge0seq  42590  meaiininc2  42632  hoicvr  42692  ovnsubaddlem2  42715  hoidmvval0  42731  hoidmvlelem3  42741  hspmbllem2  42771  vonioo  42826  vonicc  42829  smfinflem  42953  fmtnoprmfac2lem1  43556  fmtnofac1  43560  lincresunit3lem3  44357  suppdm  44393  inlinecirc02p  44602
  Copyright terms: Public domain W3C validator