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

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	ex 373	. 2 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 375	1 |- (ph -> (ps -> (ch -> th)))

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 487  ancom13s 488  3impb 829  ax11eq 1363  ax11el 1364  ssiun 2592  tz7.7 2973  onfr 2986  onint 3006  peano5 3153  eqfnfv 3797  funfvima3 3854  isocnv 3896  isotr 3897  isotrALT 3898  isomin 3899  isoini 3900  isofrlem 3901  f1oiso 3904  tfrlem11 3921  tz7.48lem 3955  abianfplem 3961  oprabvalig 4024  oalimcl 4194  oaass 4195  omwordri 4203  oewordri 4219  omsmo 4257  fundmen 4428  pw2en 4446  mapenlem2 4490  mapxpen 4495  php3 4515  php3OLD 4516  ssfi 4537  ssfiOLD 4538  isfinite2OLD 4546  unifiOLD 4557  fodomfiOLD 4566  aceq3 4733  aceq5lem5 4739  aceq5 4740  zorn2lem4 4791  zorn2lem7 4794  cardaleph 4885  alephval2 4902  axacndlem4 4962  axacndlem5 4963  axacnd 4964  mulcanpi 5027  ltrpq 5085  ltaddpr 5140  ltexprlem1 5142  ltexprlem6 5147  ltexprlem7 5148  ssgt0sr 5217  suppsr2 5223  cnegextlem2 5346  cnegext 5348  negeu 5355  receu 5701  uzwo4OLD 6210  uzwo3lem2 6217  uzwo 6455  uzwoOLD 6456  fsequb 6523  expcant 6601  expordt 6602  cau3ir 6915  faclbnd 6945  fsumcllem 7014  clm3 7079  climge0 7112  climaddlem3 7116  climmullem8 7127  climubi 7153  climsup 7155  climcau 7156  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  reccnv 7218  expcnv 7233  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag2 7259  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  infpnlem1 7506  tgclt 7624  tgss2t 7637  retopbas 7655  clsval2 7685  neindisj 7731  qdensere 7751  cnsscnp 7772  metxplem3 7828  opni3 7866  opnuni 7868  metcnp 7887  metcnpi3 7892  metcnpi4 7893  metcni2 7895  lmnn 7935  iscau3 7938  iscau4 7940  lmuni 7951  caussi 7954  lmfexlem3 7958  lmle 7960  metelcls 7965  xplm 7975  iscms2lem3 7991  cmsss 7997  bcthlem16 8014  bcthlem21 8019  bcthlem28 8026  bcthlem29 8027  bcthlem33 8031  grpidinvlem3 8050  grpidinv 8052  va1cnlem 8345  nmobndi 8438  blocnilem 8464  blocni 8465  ubthlem13 8541  htthlem12 8631  shorth 9168  projlem26 9211  pjtheu 9235  spansneleq 9493  elspansn5t 9497  pjspansnt 9500  5oalem6 9604  lnopm 9925  nmcopexlem6 9956  lnopcon 9963  nmcfnexlem6 9985  lnfncon 9990  nlelch 9994  adjlnopt 10019  leopmulit 10066  leopmul2it 10068  pjnormss 10096  pjclem4 10127  pj3s 10135  stles 10168  ssmd2 10239  dmdsl3t 10242  mdexch 10262  hatomistic 10289  cvexchlem 10295  atcv1t 10307  atcvatlem 10312  atabs 10328  mdsymlem2 10331  mdsymlem3 10332  mdsymlem5 10334  sumdmdi 10342  sumdmdlem 10345  sumdmdlem2 10346  nndivsub 10421  ee7.2a 10425  uninqs 10441  11st22nd 10458  hmphtr 10531

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