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

Theorem ee10 1366
Description: e10 28772 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 16 . 2  |-  ( ps 
->  th )
51, 4syl 15 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ceqsex  2835  moeq3  2955  reusv1  4550  reusv2lem1  4551  fveqf1o  5822  fliftcnv  5826  fliftfun  5827  undom  6966  pwdom  7029  onomeneq  7066  pwfilem  7166  ordiso  7247  ordtypelem8  7256  wdompwdom  7308  unxpwdom  7319  harwdom  7320  infeq5i  7353  cantnfcl  7384  cardiun  7631  infxpenlem  7657  dfac8b  7674  acnnum  7695  inffien  7706  dfac12lem2  7786  cdadom3  7830  cdainflem  7833  cdainf  7834  infunabs  7849  infcda  7850  infdif  7851  infdif2  7852  infmap2  7860  fictb  7887  cofsmo  7911  fin23lem21  7981  hsmexlem1  8068  iundomg  8179  iunctb  8212  fpwwe2lem9  8276  canthnum  8287  winalim2  8334  rankcf  8415  tskuni  8421  npomex  8636  hashun2  11381  limsupgord  11962  summolem2  12205  zsum  12207  isinv  13678  invsym2  13681  invfun  13682  oppcsect2  13693  oppcinv  13694  efgcpbllemb  15080  frgpuplem  15097  gsumval3  15207  1stcfb  17187  1stcrestlem  17194  2ndcdisj2  17199  txdis1cn  17345  tx1stc  17360  tgphaus  17815  divstgplem  17819  tsmsxp  17853  xmeter  17995  bndth  18472  ovolctb2  18867  ovoliunlem1  18877  i1fd  19052  dvgt0lem2  19366  taylf  19756  efcvx  19841  logccv  20026  loglesqr  20114  stadd3i  22844  strlem6  22852  dmct  23357  cnvct  23358  mptct  23360  mptctf  23363  itgmcntTMP  23603  subfaclefac  23722  erdsze2lem1  23749  erdsze2lem2  23750  snmlff  23927  prodmolem2  24158  zprod  24160  orderseqlem  24323  frrlem5c  24358  sssu  25244  islatalg  25286  basexre  25625  bwt2  25695  dualalg  25885  dualded  25886  pell1qrgaplem  27061  dnwech  27248  frgra3vlem1  28424  bnj97  29214  bnj553  29246  bnj966  29292  bnj1442  29395  dvhopellsm  31929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator