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  7469  inf3lem3  7577  epfrs  7659  karden  7811  infxpenlem  7887  iunfictbso  7987  dfac5  8001  dfac2  8003  kmlem1  8022  kmlem9  8030  infpssrlem3  8177  fin23lem25  8196  fin23lem30  8214  domtriomlem  8314  axdc3lem4  8325  axcclem  8329  zorn2lem7  8374  konigthlem  8435  wunr1om  8586  tskr1om  8634  gruen  8679  grur1a  8686  indpi  8776  genpnmax  8876  prlem934  8902  ltaddpr  8903  ltexprlem7  8911  ltaprlem  8913  axrrecex  9030  axpre-sup  9036  lelttr  9157  addid2  9241  fzind  10360  fnn0ind  10361  btwnz  10364  uzwo  10531  uzwoOLD  10532  lbzbi  10556  rpnnen1lem5  10596  xrlelttr  10738  qbtwnre  10777  xrsupsslem  10877  xrinfmsslem  10878  supxrun  10886  elfznelfzo  11184  fsequb  11306  leexp2r  11429  bernneq  11497  brfi1uzind  11707  cau3lem  12150  climuni  12338  mulcn2  12381  divalglem8  12912  ndvdssub  12919  rplpwr  13048  algcvgblem  13060  euclemma  13100  prmlem1a  13421  iscatd  13890  plelttr  14421  grpinveu  14831  efgred  15372  lspdisjb  16190  basis2  17008  0ntr  17127  uncmp  17458  1stcrest  17508  txcls  17628  txcnp  17644  tx1stc  17674  fgss2  17898  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  metcnp3  18562  reconn  18851  iscau4  19224  ellimc3  19758  ulmbdd  20306  ulmcn  20307  sinq12ge0  20408  eupai  21681  grpoinveu  21802  gxneg  21846  gxsuc  21852  gxnn0add  21854  gxadd  21855  gxnn0mul  21857  gxmul  21858  ococss  22787  shmodsi  22883  h1datomi  23075  hoaddsub  23311  adjmul  23587  chjatom  23852  atomli  23877  atcvat4i  23892  mdsymlem3  23900  mdsymlem5  23902  mdsymlem6  23903  sumdmdlem  23913  cdj3lem2a  23931  cdj3lem3a  23934  cvmsdisj  24949  dedekind  25179  fundmpss  25382  dfon2lem6  25407  dfon2lem8  25409  predpoirr  25464  predfrirr  25465  wfr3g  25529  wfrlem12  25541  frr3g  25573  frrlem11  25586  ax5seglem5  25864  ax5seg  25869  ifscgr  25970  lineext  26002  fscgr  26006  idinside  26010  btwnconn1lem11  26023  btwnconn1lem12  26024  btwnconn3  26029  brsegle  26034  seglecgr12  26037  hilbert1.2  26081  areacirc  26288  exp5d  26294  exp5j  26296  exp5k  26297  exp5l  26298  nn0prpwlem  26316  heibor1lem  26509  pridl  26638  pridlc  26672  dmnnzd  26676  prtlem11  26706  prtlem17  26716  isnacs3  26755  jm2.26  27064  sbiota1  27602  elfzelfzelfz  28093  swrdvalodm2  28160  swrdvalodm  28161  swrd0swrd  28163  swrdswrdlem  28164  swrdswrd  28165  swrdccatin1  28171  swrdccatin2  28176  swrdccatin12lem4  28179  swrdccat  28182  2cshw1lem2  28215  2cshwmod  28223  frgrancvvdeqlemB  28364  frgrawopreglem5  28374  frg2woteq  28386  tratrb  28557  onfrALT  28572  in2an  28646  pwtrrVD  28875  suctrALT2VD  28885  suctrALT2  28886  tratrbVD  28910  trintALTVD  28929  trintALT  28930  bnj1204  29318  nfsb4twAUX7  29513  nfsb4tOLD7  29682  nfsb4tw2AUXOLD7  29683  atcvrj0  30162  cvrat4  30177  athgt  30190  lplnexllnN  30298  2llnjN  30301  lvolnle3at  30316  lncmp  30517  paddclN  30576  pexmidlem4N  30707  cdleme17d3  31230  cdleme50trn2  31285  cdlemf2  31296  cdlemf  31297  cdlemj3  31557  cdlemk26b-3  31639  dihord5b  31994
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