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

Theorem ee10 1385
Description: e10 28795 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  2990  moeq3  3111  reusv1  4723  reusv2lem1  4724  fveqf1o  6029  fliftcnv  6033  fliftfun  6034  undom  7196  pwdom  7259  onomeneq  7296  pwfilem  7401  ordiso  7485  ordtypelem8  7494  wdompwdom  7546  unxpwdom  7557  harwdom  7558  infeq5i  7591  cantnfcl  7622  cardiun  7869  infxpenlem  7895  dfac8b  7912  acnnum  7933  inffien  7944  dfac12lem2  8024  cdadom3  8068  cdainflem  8071  cdainf  8072  infunabs  8087  infcda  8088  infdif  8089  infdif2  8090  infmap2  8098  fictb  8125  cofsmo  8149  fin23lem21  8219  hsmexlem1  8306  iundomg  8416  iunctb  8449  fpwwe2lem9  8513  canthnum  8524  winalim2  8571  rankcf  8652  tskuni  8658  npomex  8873  hashun2  11657  limsupgord  12266  summolem2  12510  zsum  12512  isinv  13985  invsym2  13988  invfun  13989  oppcsect2  14000  oppcinv  14001  efgcpbllemb  15387  frgpuplem  15404  gsumval3  15514  bwth  17473  1stcfb  17508  1stcrestlem  17515  2ndcdisj2  17520  txdis1cn  17667  tx1stc  17682  tgphaus  18146  divstgplem  18150  tsmsxp  18184  xmeter  18463  bndth  18983  ovolctb2  19388  ovoliunlem1  19398  i1fd  19573  dvgt0lem2  19887  taylf  20277  efcvx  20365  logccv  20554  loglesqr  20642  usgraidx2v  21412  stadd3i  23751  strlem6  23759  dmct  24106  cnvct  24107  mptct  24109  mptctf  24112  subfaclefac  24862  erdsze2lem1  24889  erdsze2lem2  24890  snmlff  25016  prodmolem2  25261  zprod  25263  orderseqlem  25527  frrlem5c  25588  pell1qrgaplem  26936  dnwech  27123  stoweid  27788  frgra3vlem1  28390  bnj97  29237  bnj553  29269  bnj966  29315  bnj1442  29418  dvhopellsm  31915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator