MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp3a Structured version   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  1374  exp3acom3r  1379  exp3acom23  1381  nfsb4tOLD  2155  ax11indn  2271  mo  2302  mopick  2342  ralrimivv  2789  mob2  3106  reuind  3129  reupick3  3618  disjiun  4194  sotr2  4524  wefrc  4568  suctrALT  4656  elpwunsn  4749  dfwe2  4754  limuni3  4824  tfisi  4830  ordom  4846  relop  5015  funcnvuni  5510  fnun  5543  mpteqb  5811  fconst5  5941  funfvima  5965  f1oweALT  6066  frxp  6448  poxp  6450  riotasv3dOLD  6591  onfununi  6595  tfrlem5  6633  tz7.48lem  6690  oecl  6773  oaordex  6793  oaass  6796  omwordri  6807  odi  6814  omass  6815  omeu  6820  oen0  6821  oewordi  6826  oewordri  6827  nnarcl  6851  nnmass  6859  dif1enOLD  7332  dif1en  7333  findcard2  7340  unblem1  7351  unblem2  7352  domunfican  7371  marypha1lem  7430  supiso  7467  inf3lem3  7575  epfrs  7657  karden  7809  infxpenlem  7885  iunfictbso  7985  dfac5  7999  dfac2  8001  kmlem1  8020  kmlem9  8028  infpssrlem3  8175  fin23lem25  8194  fin23lem30  8212  domtriomlem  8312  axdc3lem4  8323  axcclem  8327  zorn2lem7  8372  konigthlem  8433  wunr1om  8584  tskr1om  8632  gruen  8677  grur1a  8684  indpi  8774  genpnmax  8874  prlem934  8900  ltaddpr  8901  ltexprlem7  8909  ltaprlem  8911  axrrecex  9028  axpre-sup  9034  lelttr  9155  addid2  9239  fzind  10358  fnn0ind  10359  btwnz  10362  uzwo  10529  uzwoOLD  10530  lbzbi  10554  rpnnen1lem5  10594  xrlelttr  10736  qbtwnre  10775  xrsupsslem  10875  xrinfmsslem  10876  supxrun  10884  elfznelfzo  11182  fsequb  11304  leexp2r  11427  bernneq  11495  brfi1uzind  11705  cau3lem  12148  climuni  12336  mulcn2  12379  divalglem8  12910  ndvdssub  12917  rplpwr  13046  algcvgblem  13058  euclemma  13098  prmlem1a  13419  iscatd  13888  plelttr  14419  grpinveu  14829  efgred  15370  lspdisjb  16188  basis2  17006  0ntr  17125  uncmp  17456  1stcrest  17506  txcls  17626  txcnp  17642  tx1stc  17672  fgss2  17896  alexsubALTlem2  18069  alexsubALTlem3  18070  alexsubALTlem4  18071  metcnp3  18560  reconn  18849  iscau4  19222  ellimc3  19756  ulmbdd  20304  ulmcn  20305  sinq12ge0  20406  eupai  21679  grpoinveu  21800  gxneg  21844  gxsuc  21850  gxnn0add  21852  gxadd  21853  gxnn0mul  21855  gxmul  21856  ococss  22785  shmodsi  22881  h1datomi  23073  hoaddsub  23309  adjmul  23585  chjatom  23850  atomli  23875  atcvat4i  23890  mdsymlem3  23898  mdsymlem5  23900  mdsymlem6  23901  sumdmdlem  23911  cdj3lem2a  23929  cdj3lem3a  23932  cvmsdisj  24947  dedekind  25177  fundmpss  25378  dfon2lem6  25403  dfon2lem8  25405  predpoirr  25457  predfrirr  25458  wfr3g  25522  wfrlem12  25534  frr3g  25546  frrlem11  25559  ax5seglem5  25837  ax5seg  25842  ifscgr  25943  lineext  25975  fscgr  25979  idinside  25983  btwnconn1lem11  25996  btwnconn1lem12  25997  btwnconn3  26002  brsegle  26007  seglecgr12  26010  hilbert1.2  26054  areacirc  26251  exp5d  26257  exp5j  26259  exp5k  26260  exp5l  26261  nn0prpwlem  26279  heibor1lem  26472  pridl  26601  pridlc  26635  dmnnzd  26639  prtlem11  26669  prtlem17  26679  isnacs3  26718  jm2.26  27027  sbiota1  27566  elfzelfzelfz  28057  swrdvalodm2  28124  swrdvalodm  28125  swrd0swrd  28127  swrdswrdlem  28128  swrdswrd  28129  swrdccatin1  28135  swrdccatin2  28140  swrdccatin12lem4  28143  swrdccat  28146  2cshw1lem2  28179  2cshwmod  28187  frgrancvvdeqlemB  28328  frgrawopreglem5  28338  frg2woteq  28350  tratrb  28521  onfrALT  28536  in2an  28610  pwtrrVD  28839  suctrALT2VD  28849  suctrALT2  28850  tratrbVD  28874  trintALTVD  28893  trintALT  28894  bnj1204  29282  nfsb4twAUX7  29477  nfsb4tOLD7  29646  nfsb4tw2AUXOLD7  29647  atcvrj0  30126  cvrat4  30141  athgt  30154  lplnexllnN  30262  2llnjN  30265  lvolnle3at  30280  lncmp  30481  paddclN  30540  pexmidlem4N  30671  cdleme17d3  31194  cdleme50trn2  31249  cdlemf2  31260  cdlemf  31261  cdlemj3  31521  cdlemk26b-3  31603  dihord5b  31958
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