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

Theorem exp3a 426
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
exp3a  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem exp3a
StepHypRef Expression
1 exp3a.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 29 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 424 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 75 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  expdimp  427  pm3.3  432  syland  468  exp32  589  exp4c  592  exp4d  593  exp42  595  exp44  597  exp5c  600  impl  604  mpan2d  656  3impib  1151  exp5o  1172  exbir  1371  exp3acom3r  1376  exp3acom23  1378  nfsb4t  2129  ax11indn  2245  mo  2276  mopick  2316  ralrimivv  2757  mob2  3074  reuind  3097  reupick3  3586  disjiun  4162  sotr2  4492  wefrc  4536  suctr  4624  elpwunsn  4716  dfwe2  4721  limuni3  4791  tfisi  4797  ordom  4813  relop  4982  funcnvuni  5477  fnun  5510  mpteqb  5778  fconst5  5908  funfvima  5932  f1oweALT  6033  frxp  6415  poxp  6417  riotasv3dOLD  6558  onfununi  6562  tfrlem5  6600  tz7.48lem  6657  oecl  6740  oaordex  6760  oaass  6763  omwordri  6774  odi  6781  omass  6782  omeu  6787  oen0  6788  oewordi  6793  oewordri  6794  nnarcl  6818  nnmass  6826  dif1enOLD  7299  dif1en  7300  findcard2  7307  unblem1  7318  unblem2  7319  domunfican  7338  marypha1lem  7396  supiso  7433  inf3lem3  7541  epfrs  7623  karden  7775  infxpenlem  7851  iunfictbso  7951  dfac5  7965  dfac2  7967  kmlem1  7986  kmlem9  7994  infpssrlem3  8141  fin23lem25  8160  fin23lem30  8178  domtriomlem  8278  axdc3lem4  8289  axcclem  8293  zorn2lem7  8338  konigthlem  8399  wunr1om  8550  tskr1om  8598  gruen  8643  grur1a  8650  indpi  8740  genpnmax  8840  prlem934  8866  ltaddpr  8867  ltexprlem7  8875  ltaprlem  8877  axrrecex  8994  axpre-sup  9000  lelttr  9121  addid2  9205  fzind  10324  fnn0ind  10325  btwnz  10328  uzwo  10495  uzwoOLD  10496  lbzbi  10520  rpnnen1lem5  10560  xrlelttr  10702  qbtwnre  10741  xrsupsslem  10841  xrinfmsslem  10842  supxrun  10850  elfznelfzo  11147  fsequb  11269  leexp2r  11392  bernneq  11460  brfi1uzind  11670  cau3lem  12113  climuni  12301  mulcn2  12344  divalglem8  12875  ndvdssub  12882  rplpwr  13011  algcvgblem  13023  euclemma  13063  prmlem1a  13384  iscatd  13853  plelttr  14384  grpinveu  14794  efgred  15335  lspdisjb  16153  basis2  16971  0ntr  17090  uncmp  17420  1stcrest  17469  txcls  17589  txcnp  17605  tx1stc  17635  fgss2  17859  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  metcnp3  18523  reconn  18812  iscau4  19185  ellimc3  19719  ulmbdd  20267  ulmcn  20268  sinq12ge0  20369  eupai  21642  grpoinveu  21763  gxneg  21807  gxsuc  21813  gxnn0add  21815  gxadd  21816  gxnn0mul  21818  gxmul  21819  ococss  22748  shmodsi  22844  h1datomi  23036  hoaddsub  23272  adjmul  23548  chjatom  23813  atomli  23838  atcvat4i  23853  mdsymlem3  23861  mdsymlem5  23863  mdsymlem6  23864  sumdmdlem  23874  cdj3lem2a  23892  cdj3lem3a  23895  cvmsdisj  24910  dedekind  25140  fundmpss  25336  dfon2lem6  25358  dfon2lem8  25360  predpoirr  25411  predfrirr  25412  wfr3g  25469  wfrlem12  25481  frr3g  25494  frrlem11  25507  ax5seglem5  25776  ax5seg  25781  ifscgr  25882  lineext  25914  fscgr  25918  idinside  25922  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn3  25941  brsegle  25946  seglecgr12  25949  hilbert1.2  25993  areacirc  26187  exp5d  26193  exp5j  26195  exp5k  26196  exp5l  26197  nn0prpwlem  26215  heibor1lem  26408  pridl  26537  pridlc  26571  dmnnzd  26575  prtlem11  26605  prtlem17  26615  isnacs3  26654  jm2.26  26963  sbiota1  27502  elfzelfzelfz  27981  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin12c  28028  frgrancvvdeqlemB  28141  frgrawopreglem5  28151  frg2woteq  28163  tratrb  28331  onfrALT  28346  in2an  28418  pwtrrVD  28647  suctrALT2VD  28657  suctrALT2  28658  tratrbVD  28682  trintALTVD  28701  trintALT  28702  bnj1204  29087  nfsb4twAUX7  29280  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  atcvrj0  29910  cvrat4  29925  athgt  29938  lplnexllnN  30046  2llnjN  30049  lvolnle3at  30064  lncmp  30265  paddclN  30324  pexmidlem4N  30455  cdleme17d3  30978  cdleme50trn2  31033  cdlemf2  31044  cdlemf  31045  cdlemj3  31305  cdlemk26b-3  31387  dihord5b  31742
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 178  df-an 361
  Copyright terms: Public domain W3C validator