Theorem exp32 294

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  exp44 302  exp45 303  adantrll 316  adantrlr 317  adantrrl 318  adantrrr 319  anassrs 338  3impb 610  ssiun 2018  wefrc 2195  tz7.7 2224  onfr 2237  onint 2261  peano5 2394  cleqfv 2880  funfvima3 2906  isocnv 2934  isotr 2935  isotrALT 2936  isomin 2937  isoini 2938  isofrlem 2939  isowe 2941  f1oiso 2942  tfrlem8 2956  tfrlem11 2959  tz7.48lem 2993  abianfplem 2999  oprabvalig 3048  oalimcl 3162  oaass 3163  omsmo 3196  fundmen 3333  pw2en 3348  mapenlem2 3385  mapxpen 3390  php3 3411  ssfi 3430  isfinite2 3437  aceq3 3556  aceq5lem5 3562  aceq5 3563  zornlem4 3606  zornlem7 3609  cardaleph 3690  axacndlem4 3756  axacndlem5 3757  axacnd 3758  mulcanpi 3821  ltrpq 3879  ltaddpr 3934  ltexprlem1 3936  ltexprlem6 3941  ltexprlem7 3942  ssgt0sr 4011  suppsr2 4017  negeu 4124  receu 4215  uzwo 4605  nnwoOLD 4608  uzwo3lem2 4615  shorth 5176  projlem26 5218  pjthu 5241  pjthu2 5242  shscl 5282  spansneleq 5475  elspansn5t 5479  5oalem6 5549  pjnormss 5638  pjclem4 5653  pj3s 5659  stles 5682  ssmd2 5735  hatomistic 5755  cvexchlem 5759  atcv1 5768  atcvatlem 5770  mdsymlem2 5777  mdsymlem3 5778  mdsymlem5 5780  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org