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

Theorem 3ad2antl1 1150
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl1
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantlr 714 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl2 1145 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  smorndom  6827  omeulem1  7019  dif1enOLD  7542  dif1en  7543  ordiso2  7727  infpssrlem4  8473  fin1a2lem9  8575  gchpwdom  8835  tskwun  8949  gruxp  8972  fzo1fzo0n0  11586  muldvds2  13556  dvds2add  13562  dvds2sub  13563  dvdstr  13564  mulgnnsubcl  15637  mulgpropd  15658  gexdvdsi  16080  rngidss  16669  reslmhm2  17132  issubassa  17393  obs2ss  18152  lsslindf  18257  mndvcl  18289  mhmvlin  18295  madurid  18448  restntr  18784  cnpnei  18866  upxp  19194  qtopss  19286  opnfbas  19413  fbasrn  19455  trfg  19462  ufilmax  19478  ustuqtop1  19814  prdsxmetlem  19941  nmoix  20306  nmoi2  20307  iimulcl  20507  mbfimaopn2  21133  lgsval4lem  22644  f1otrg  23115  brbtwn2  23149  colinearalg  23154  axsegconlem1  23161  redwlk  23503  gxcl  23750  lnosub  24157  pjspansn  24978  eulerpartlemb  26749  cnpcon  27117  ghomf1olem  27311  nodenselem8  27827  mblfinlem2  28426  mblfinlem3  28427  mettrifi  28650  ghomdiv  28746  grpokerinj  28747  rngohomco  28777  crngohomfo  28803  keridl  28829  mzpsubst  29082  lzunuz  29103  diophrex  29111  rmxycomplete  29255  jm2.26  29348  lnmepi  29435  lmhmlnmsplit  29437  fmul01lt1  29764  stoweidlem60  29852  wallispilem3  29859  vdn1frgrav2  30615  usg2spot2nb  30655  numclwlk1lem2fo  30685  fsuppmapnn0fiub  30796  lincresunit3lem3  31005  cvrcon3b  32919
  Copyright terms: Public domain W3C validator