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 489  ancom13s 490  3impb 832  ax11eq 1396  ax11el 1397  ssiun 2641  tz7.7 3028  onfr 3041  onint 3061  peano5 3215  eqfnfv 3873  funfvima3 3930  isocnv 3972  isotr 3973  isotrALT 3974  isomin 3975  isoini 3976  isofrlem 3977  f1oiso 3980  tfrlem11 3997  tz7.48lem 4031  abianfplem 4037  oprabvalig 4101  oalimcl 4278  oaass 4279  omwordri 4287  oewordri 4303  omsmo 4341  fundmen 4515  pw2en 4533  mapenlem2 4579  mapxpen 4584  php3 4604  ssfi 4625  unifi 4642  fodomfi 4650  aceq3 4819  aceq5lem5 4825  aceq5 4826  zorn2lem4 4877  zorn2lem7 4880  cardaleph 4974  alephval2 4991  axacndlem4 5051  axacndlem5 5052  axacnd 5053  mulcanpi 5116  ltrpq 5174  ltaddpr 5229  ltexprlem1 5231  ltexprlem6 5236  ltexprlem7 5237  ssgt0sr 5306  suppsr2 5312  cnegexlem2 5435  cnegex 5437  negeui 5444  receui 5787  uzwo4OLD 6323  uzwo3lem2 6330  uzwo 6515  uzwoOLD 6516  fsequb 6583  expcan 6723  expord 6724  cau3iri 7038  faclbnd 7068  fsumcllem 7137  clm3i 7202  climge0 7235  climaddlem3 7239  climmullem8 7250  climubii 7276  climsupi 7278  climcaui 7279  caucvglem6 7285  caucvgi 7286  serzf0i 7292  ser1f0i 7293  reccnv 7341  expcnv 7356  cvgratlem5 7377  fsum0diaglem2 7380  fsum0diag2 7382  acdc3 7612  acdc2 7615  acdc5 7618  acdc 7620  infpnlem1 7631  tgcl 7748  tgss2 7761  retopbas 7775  clsval2 7805  neindisj 7851  qdensere 7871  cnsscnp 7892  metxplem3 7948  opni3 7986  opnuni 7988  metcnp 8007  metcnpi3 8012  metcnpi4 8013  metcni2 8015  lmnn 8055  iscau3 8058  iscau4 8060  lmuni 8071  caussi 8074  lmfexlem3 8078  lmle 8080  metelcls 8085  xplm 8095  iscms2lem3 8111  cmsss 8117  bcthlem16 8134  bcthlem21 8139  bcthlem28 8146  bcthlem29 8147  bcthlem33 8151  grpidinvlem3 8170  grpidinv 8172  va1cnlem 8464  nmobndi 8557  blocnilem 8583  blocni 8584  ubthlem13 8660  htthlem12 8750  shorth 9288  projlem26 9331  pjtheui 9355  spansneleq 9613  elspansn5 9617  pjspansn 9620  5oalem6 9724  lnopmi 10042  nmcopexlem6 10073  lnopconi 10080  nmcfnexlem6 10102  lnfnconi 10107  nlelchi 10111  adjlnop 10136  leopmuli 10183  leopmul2i 10185  pjnormssi 10213  pjclem4 10245  pj3si 10253  stlesi 10286  ssmd2 10357  dmdsl3 10360  mdexchi 10380  hatomistici 10407  cvexchlem 10413  atcv1 10425  atcvatlem 10430  atabsi 10446  mdsymlem2 10449  mdsymlem3 10450  mdsymlem5 10452  sumdmdii 10460  sumdmdlem 10463  sumdmdlem2 10464  nndivsub 10544  ee7.2a 10548  uninqs 10563  uninqsOLD 10564  11st22nd 10576  hmphtr 10667

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