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 828  ax11eq 1362  ax11el 1363  ssiun 2588  tz7.7 2969  onfr 2982  onint 3002  peano5 3149  eqfnfv 3792  funfvima3 3849  isocnv 3891  isotr 3892  isotrALT 3893  isomin 3894  isoini 3895  isofrlem 3896  f1oiso 3899  tfrlem11 3916  tz7.48lem 3950  abianfplem 3956  oprabvalig 4019  oalimcl 4187  oaass 4188  omwordri 4196  oewordri 4212  omsmo 4250  fundmen 4418  pw2en 4435  mapenlem2 4479  mapxpen 4484  php3 4504  ssfi 4524  isfinite2 4532  unifi 4541  fodomfi 4549  aceq3 4716  aceq5lem5 4722  aceq5 4723  zorn2lem4 4774  zorn2lem7 4777  cardaleph 4868  alephval2 4885  axacndlem4 4945  axacndlem5 4946  axacnd 4947  mulcanpi 5010  ltrpq 5068  ltaddpr 5123  ltexprlem1 5125  ltexprlem6 5130  ltexprlem7 5131  ssgt0sr 5200  suppsr2 5206  cnegextlem2 5329  cnegext 5331  negeu 5338  receu 5680  uzwo4OLD 6168  uzwo3lem2 6175  uzwo 6400  uzwoOLD 6401  fsequb 6468  expcant 6546  expordt 6547  cau3ir 6867  faclbnd 6897  fsumcllem 6967  clm3 7032  climge0 7065  climaddlem3 7069  climmullem8 7080  climubi 7106  climsup 7108  climcau 7109  caucvglem6 7115  caucvg 7116  serzf0 7122  ser1f0 7123  reccnv 7170  expcnv 7185  cvgratlem5 7206  fsum0diaglem2 7209  fsum0diag2 7211  acdc3 7446  acdc2 7449  acdc5 7452  acdc 7454  infpnlem1 7466  tgclt 7584  tgss2t 7597  retopbas 7615  clsval2 7645  neindisj 7691  qdensere 7711  cnsscnp 7732  metxplem3 7790  opni3 7828  opnuni 7830  metcnp 7849  metcnpi3 7854  metcnpi4 7855  metcni2 7857  lmnn 7897  iscau3 7900  iscau4 7902  lmuni 7913  caussi 7916  lmfexlem3 7920  lmle 7922  metelcls 7927  xplm 7937  iscms2lem3 7953  cmsss 7959  bcthlem16 7976  bcthlem21 7981  bcthlem28 7988  bcthlem29 7989  bcthlem33 7993  grpidinvlem3 8012  grpidinv 8014  va1cnlem 8307  nmobndi 8398  blocnilem 8423  blocni 8424  ubthlem13 8500  htthlem12 8589  shorth 9123  projlem26 9166  pjtheu 9190  spansneleq 9449  spansneleqOLD 9450  elspansn5t 9454  pjspansnt 9457  5oalem6 9561  lnopm 9881  nmcopexlem6 9912  lnopcon 9919  nmcfnexlem6 9941  lnfncon 9946  nlelch 9950  adjlnopt 9975  leopmulit 10022  leopmul2it 10024  pjnormss 10052  pjclem4 10083  pj3s 10091  stles 10124  ssmd2 10195  dmdsl3t 10198  mdexch 10218  hatomistic 10245  cvexchlem 10251  atcv1t 10263  atcvatlem 10268  atabs 10284  mdsymlem2 10287  mdsymlem3 10288  mdsymlem5 10290  sumdmdi 10298  sumdmdlem 10301  sumdmdlem2 10302  nndivsub 10379  ee7.2a 10383  uninqs 10400  11st22nd 10412  hmphtr 10477

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