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

Theorem ee10 1366
Description: e10 28467 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  2822  moeq3  2942  reusv1  4534  reusv2lem1  4535  fveqf1o  5806  fliftcnv  5810  fliftfun  5811  undom  6950  pwdom  7013  onomeneq  7050  pwfilem  7150  ordiso  7231  ordtypelem8  7240  wdompwdom  7292  unxpwdom  7303  harwdom  7304  infeq5i  7337  cantnfcl  7368  cardiun  7615  infxpenlem  7641  dfac8b  7658  acnnum  7679  inffien  7690  dfac12lem2  7770  cdadom3  7814  cdainflem  7817  cdainf  7818  infunabs  7833  infcda  7834  infdif  7835  infdif2  7836  infmap2  7844  fictb  7871  cofsmo  7895  fin23lem21  7965  hsmexlem1  8052  iundomg  8163  iunctb  8196  fpwwe2lem9  8260  canthnum  8271  winalim2  8318  rankcf  8399  tskuni  8405  npomex  8620  hashun2  11365  limsupgord  11946  summolem2  12189  zsum  12191  isinv  13662  invsym2  13665  invfun  13666  oppcsect2  13677  oppcinv  13678  efgcpbllemb  15064  frgpuplem  15081  gsumval3  15191  1stcfb  17171  1stcrestlem  17178  2ndcdisj2  17183  txdis1cn  17329  tx1stc  17344  tgphaus  17799  divstgplem  17803  tsmsxp  17837  xmeter  17979  bndth  18456  ovolctb2  18851  ovoliunlem1  18861  i1fd  19036  dvgt0lem2  19350  taylf  19740  efcvx  19825  logccv  20010  loglesqr  20098  stadd3i  22828  strlem6  22836  dmct  23342  cnvct  23343  mptct  23345  mptctf  23348  itgmcntTMP  23588  subfaclefac  23707  erdsze2lem1  23734  erdsze2lem2  23735  snmlff  23912  orderseqlem  24252  frrlem5c  24287  sssu  25141  islatalg  25183  basexre  25522  bwt2  25592  dualalg  25782  dualded  25783  pell1qrgaplem  26958  dnwech  27145  frgra3vlem1  28178  bnj97  28898  bnj553  28930  bnj966  28976  bnj1442  29079  dvhopellsm  31307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator