HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem exp32 377
Description: An exportation inference.
Hypothesis
Ref Expression
exp32.1 |- ((ph /\ (ps /\ ch)) -> th)
Assertion
Ref Expression
exp32 |- (ph -> (ps -> (ch -> th)))
Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3 |- ((ph /\ (ps /\ ch)) -> th)
21ex 373 . 2 |- (ph -> ((ps /\ ch) -> th))
32exp3a 375 1 |- (ph -> (ps -> (ch -> th)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  exp44 385  exp45 386  adantrll 400  adantrlr 401  adantrrl 402  adantrrr 403  anassrs 441  ancom2s 486  ancom13s 487  3impb 827  ax11eq 1356  ax11el 1357  ssiun 2582  tz7.7 2963  onfr 2976  onint 2996  peano5 3143  eqfnfv 3782  funfvima3 3839  isocnv 3881  isotr 3882  isotrALT 3883  isomin 3884  isoini 3885  isofrlem 3886  f1oiso 3889  tfrlem11 3906  tz7.48lem 3940  abianfplem 3946  oprabvalig 4009  oalimcl 4178  oaass 4179  omwordri 4187  oewordri 4203  omsmo 4241  fundmen 4409  pw2en 4426  mapenlem2 4470  mapxpen 4475  php3 4495  ssfi 4515  isfinite2 4523  unifi 4532  fodomfi 4540  aceq3 4705  aceq5lem5 4711  aceq5 4712  zorn2lem4 4763  zorn2lem7 4766  cardaleph 4857  alephval2 4874  axacndlem4 4934  axacndlem5 4935  axacnd 4936  mulcanpi 4999  ltrpq 5057  ltaddpr 5112  ltexprlem1 5114  ltexprlem6 5119  ltexprlem7 5120  ssgt0sr 5189  suppsr2 5195  cnegextlem2 5318  cnegext 5320  negeu 5327  receu 5670  uzwo4OLD 6158  uzwo3lem2 6165  uzwo 6387  uzwoOLD 6388  fsequb 6455  expcant 6532  expordt 6533  cau3ir 6852  faclbnd 6882  fsumcllem 6952  clm3 7017  climge0 7049  climaddlem3 7052  climmullem8 7063  climubi 7089  climsup 7091  climcau 7092  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  reccnv 7153  expcnv 7168  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag2 7194  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  infpnlem1 7449  tgclt 7566  tgss2t 7579  retopbas 7597  clsval2 7627  neindisj 7672  qdensere 7691  cnsscnp 7711  metxplem3 7768  opni3 7806  opnuni 7808  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcni2 7834  lmnn 7873  iscau3 7876  lmuni 7886  caussi 7889  lmfexlem3 7893  lmle 7895  metelcls 7900  xplm 7909  iscms2lem3 7925  cmsss 7931  bcthlem16 7948  bcthlem21 7953  bcthlem28 7960  bcthlem29 7961  bcthlem33 7965  grpidinvlem3 7984  grpidinv 7986  va1cnlem 8279  nmobndi 8370  blocnilem 8395  blocni 8396  ubthlem13 8472  htthlem12 8561  shorth 9084  projlem26 9127  pjtheu 9150  spansneleq 9409  spansneleqOLD 9410  elspansn5t 9414  pjspansnt 9417  5oalem6 9521  lnopm 9840  nmcopexlem6 9871  lnopcon 9878  nmcfnexlem6 9900  lnfncon 9905  nlelch 9909  adjlnopt 9934  leopmulit 9978  leopmul2it 9980  pjnormss 10007  pjclem4 10037  pj3s 10045  stles 10078  ssmd2 10147  dmdsl3t 10150  mdexch 10170  hatomistic 10197  cvexchlem 10203  atcv1t 10215  atcvatlem 10220  atabs 10236  mdsymlem2 10239  mdsymlem3 10240  mdsymlem5 10242  sumdmdi 10249  sumdmdlem 10252  sumdmdlem2 10253  uninqs 10342  11st22nd 10354  hmphtr 10418
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain