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

Theorem 3ad2antl1 1117
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 695 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl2 1112 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  smorndom  6401  omeulem1  6596  dif1enOLD  7106  dif1en  7107  ordiso2  7246  infpssrlem4  7948  fin1a2lem9  8050  gchpwdom  8312  tskwun  8422  gruxp  8445  muldvds2  12570  dvds2add  12576  dvds2sub  12577  dvdstr  12578  mulgnnsubcl  14595  mulgpropd  14616  gexdvdsi  14910  rngidss  15383  reslmhm2  15826  issubassa  16080  obs2ss  16645  restntr  16928  cnpnei  17009  upxp  17333  qtopss  17422  opnfbas  17553  fbasrn  17595  trfg  17602  ufilmax  17618  prdsxmetlem  17948  nmoix  18254  nmoi2  18255  iimulcl  18451  mbfimaopn2  19028  lgsval4lem  20562  gxcl  20948  lnosub  21353  pjspansn  22172  cnpcon  23776  ghomf1olem  24016  nodenselem8  24413  brbtwn2  24605  colinearalg  24610  axsegconlem1  24617  11st22nd  25148  prjmapcp  25268  isppm  25457  rltrran  25517  istopxc  25651  lvsovso  25729  mettrifi  26576  ghomdiv  26677  grpokerinj  26678  rngohomco  26708  crngohomfo  26734  keridl  26760  mzpsubst  26929  lzunuz  26950  diophrex  26958  rmxycomplete  27105  jm2.26  27198  lnmepi  27286  lmhmlnmsplit  27288  lsslindf  27403  mndvcl  27549  mhmvlin  27555  fmul01lt1  27819  redwlk  28364  lub0N  30001  glb0N  30005  cvrcon3b  30089
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator