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 371	. 2 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 374	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  exp44 385  exp45 386  adantrll 400  adantrlr 401  adantrrl 402  adantrrr 403  anassrs 443  ancom2s 490  ancom13s 491  3impb 835  ax11eq 1402  ax11el 1403  ssiun 2660  tz7.7 3001  onfr 3014  onint 3152  peano5 3241  eqfnfv 3909  funfvima3 3968  isocnv 4010  isotr 4011  isotrALT 4012  isomin 4013  isoini 4014  isofrlem 4015  f1oiso 4018  oprabvalig 4084  tfrlem11 4222  tz7.48lem 4256  abianfplem 4262  oalimcl 4330  oaass 4331  omwordri 4339  oewordri 4355  omsmo 4397  fundmen 4569  pw2en 4587  mapenlem2 4637  mapxpen 4642  php3 4662  ssfi 4683  unifi 4701  fodomfi 4709  aceq3 4879  aceq5lem5 4885  aceq5 4886  zorn2lem4 4937  zorn2lem7 4940  cardaleph 5035  alephval2 5052  axacndlem4 5116  axacndlem5 5117  axacnd 5118  mulcanpi 5181  ltrpq 5239  ltaddpr 5294  ltexprlem1 5296  ltexprlem6 5301  ltexprlem7 5302  ssgt0sr 5371  suppsr2 5377  cnegexlem2 5500  cnegex 5502  negeui 5509  receui 5853  uzwo4OLD 6381  uzwo3lem2 6389  uzwo 6582  uzwoOLD 6583  fsequb 6654  expcan 6798  expord 6799  cau3iri 7118  faclbnd 7148  fsumcllem 7217  clm3i 7282  climge0 7315  climaddlem3 7319  climmullem8 7330  climubii 7356  climsupi 7358  climcaui 7359  caucvglem6 7365  caucvgi 7366  serzf0i 7372  reccnv 7422  expcnv 7437  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag2 7464  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  infpnlem1 7718  tgcl 7836  tgss2 7849  retopbas 7865  clsval2 7895  neindisj 7941  qdensere 7961  cnsscnp 7982  metxplem3 8038  opni3 8076  opnuni 8078  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni2 8106  lmnn 8146  iscau3 8149  iscau4 8151  lmuni 8162  caussi 8165  lmfexlem3 8169  lmle 8171  metelcls 8176  xplm 8186  iscms2lem3 8202  cmsss 8208  bcthlem16 8225  bcthlem21 8230  bcthlem28 8237  bcthlem29 8238  bcthlem33 8242  grpidinvlem3 8263  grpidinv 8265  vacnlem3 8584  va1cnlem 8599  nmobndi 8692  blocnilem 8719  blocni 8720  ubthlem13 8800  ubthlem13OLD 8801  htthlem12 8893  shorth 9444  projlem26 9487  pjtheui 9511  spansneleq 9769  elspansn5 9773  pjspansn 9776  5oalem6 9882  lnopmi 10204  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem6 10264  lnfnconi 10269  nlelchi 10273  adjlnop 10298  leopmuli 10346  leopmul2i 10348  pjnormssi 10376  pjclem4 10408  pj3si 10416  stlesi 10449  ssmd2 10520  dmdsl3 10523  mdexchi 10543  hatomistici 10570  cvexchlem 10576  atcv1 10589  atcvatlem 10594  atabsi 10610  mdsymlem2 10613  mdsymlem3 10614  mdsymlem5 10616  sumdmdii 10624  sumdmdlem 10627  sumdmdlem2 10628  nndivsub 10706  ee7.2a 10710  uninqs 10730  11st22nd 10742  hmphtr 11037  expr 11361  fictblem 11422  fictb 11423  inficlALT 11424  ordtypelem4 11430  hartoglem 11435  hartog 11436  omsublim 11448  omsubinit 11451  cnpnei 11472  cnntr 11474  subcls 11481  subntr 11482  uncomp 11490  hscptsscld 11491  alexsublem3 11498  alexsublem4 11499  alexsub 11500  subtopmet 11506  reconnlem4 11510  2ndc1stc 11538  2ndcctbss 11539  fnetr 11556  reftr 11558  lfinpfin 11574  locfincomp 11575  comppfsc 11578  neibastop2 11584  neibastop3 11585  fnemeet1 11589  fnejoin1 11591  ist1-2 11603  fbunfip 11631  extbas1 11641  filrn 11643  isufil2 11650  filssufillem 11655  limfilcf 11683  elfilmap 11690  elfilmap2 11691  elfilmap3 11692  rnelfmlem 11698  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem2 11701  fmfnfmlem3 11702  fmfnfmlem4 11703  fmufil 11705  flimfbas 11713  fclusnei 11719  fclusneii 11721  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnp 11730  fcluscomplem 11732  fclusfnei 11738  tailfb 11762  filbcmb 11857  ismtyhmeolem 12006  heiborlem19 12029  rrncms 12075

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 145  df-an 223

Copyright terms: Public domain