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

Theorem ee10 1382
Description: e10 28504 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) TODO: this is frequently used; come up with better label.
Hypotheses
Ref Expression
ee10.1  |-  ( ph  ->  ps )
ee10.2  |-  ch
ee10.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
ee10  |-  ( ph  ->  th )

Proof of Theorem ee10
StepHypRef Expression
1 ee10.1 . 2  |-  ( ph  ->  ps )
2 ee10.2 . . 3  |-  ch
3 ee10.3 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
42, 3mpi 17 . 2  |-  ( ps 
->  th )
51, 4syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ceqsex  2950  moeq3  3071  reusv1  4682  reusv2lem1  4683  fveqf1o  5988  fliftcnv  5992  fliftfun  5993  undom  7155  pwdom  7218  onomeneq  7255  pwfilem  7359  ordiso  7441  ordtypelem8  7450  wdompwdom  7502  unxpwdom  7513  harwdom  7514  infeq5i  7547  cantnfcl  7578  cardiun  7825  infxpenlem  7851  dfac8b  7868  acnnum  7889  inffien  7900  dfac12lem2  7980  cdadom3  8024  cdainflem  8027  cdainf  8028  infunabs  8043  infcda  8044  infdif  8045  infdif2  8046  infmap2  8054  fictb  8081  cofsmo  8105  fin23lem21  8175  hsmexlem1  8262  iundomg  8372  iunctb  8405  fpwwe2lem9  8469  canthnum  8480  winalim2  8527  rankcf  8608  tskuni  8614  npomex  8829  hashun2  11612  limsupgord  12221  summolem2  12465  zsum  12467  isinv  13940  invsym2  13943  invfun  13944  oppcsect2  13955  oppcinv  13956  efgcpbllemb  15342  frgpuplem  15359  gsumval3  15469  1stcfb  17461  1stcrestlem  17468  2ndcdisj2  17473  txdis1cn  17620  tx1stc  17635  tgphaus  18099  divstgplem  18103  tsmsxp  18137  xmeter  18416  bndth  18936  ovolctb2  19341  ovoliunlem1  19351  i1fd  19526  dvgt0lem2  19840  taylf  20230  efcvx  20318  logccv  20507  loglesqr  20595  usgraidx2v  21365  stadd3i  23704  strlem6  23712  dmct  24059  cnvct  24060  mptct  24062  mptctf  24065  subfaclefac  24815  erdsze2lem1  24842  erdsze2lem2  24843  snmlff  24969  prodmolem2  25214  zprod  25216  orderseqlem  25466  frrlem5c  25501  pell1qrgaplem  26826  dnwech  27013  stoweid  27679  frgra3vlem1  28104  bnj97  28943  bnj553  28975  bnj966  29021  bnj1442  29124  dvhopellsm  31600
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator