Theorem exp3a 292

Description: Exportation deduction.

Hypothesis

Ref	Expression
exp3a.1	|- (ph -> ((ps /\ ch) -> th))

Assertion

Ref	Expression
exp3a	|- (ph -> (ps -> (ch -> th)))

Proof of Theorem exp3a

Step	Hyp	Ref	Expression
1		exp3a.1	. 2 |- (ph -> ((ps /\ ch) -> th))
2		impexp 276	. 2 |- (((ps /\ ch) -> th) <-> (ps -> (ch -> th)))
3	1, 2	sylib 173	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  exp32 294  exp4b 296  exp4c 297  exp4d 298  exp42 300  exp44 302  imdistan 339  syland 352  anabsi7 379  mpani 521  mpan2i 522  mpand 524  mpan2d 525  pclem6 555  mopick 1054  r19.21aivv 1263  r19.23advv 1288  reupick 1578  dedth3h 1788  pwssun 1917  reuuni1 1955  trel 2048  supnub 2162  frirr 2176  wefrc 2195  ordelord 2221  tz7.7 2224  ordsseleq 2227  ordtr2 2257  oneqmini 2272  trsuc 2308  ordom 2382  ralxp 2456  weinxp 2467  relss 2480  funcnvuni 2706  fnun 2730  funfvima 2904  f1oweOLD 2944  tfrlem5 2953  tz7.48lem 2993  tz7.49 2997  abianfp 3000  oecl 3140  oaordex 3160  oaass 3163  oen0 3165  nnarcl 3174  nndi 3180  nnmass 3181  nnmord 3189  nnmcan 3190  omsmolem 3195  omsmo 3196  3ecoptocl 3241  unen 3338  sdomen2 3380  mapenlem2 3385  xpmapenlem4 3394  sucdomi 3419  unblem1 3431  unblem2 3432  fiint 3445  inf3lem2 3465  inf3lem3 3466  inf3lem6 3469  zfregs 3491  r1ord 3499  karden 3551  aceq5lem5 3562  aceq5 3563  aceq6b 3565  kmlem1 3580  kmlem8 3587  numthlem 3598  zornlem7 3609  sucdom 3648  indpi 3828  genpnmax 3904  ltaddpr 3934  ltexprlem7 3942  ltaprlem 3944  prlem936b 3948  prlem936 3949  suplem1pr 3955  ssgt0sr 4011  axrecex 4079  addsubt 4151  lelttrt 4289  ltletrt 4290  letrt 4291  nnleltp1t 4448  elnnz1 4581  uzwo 4605  nnwoOLD 4608  btwnz 4613  uzwo3lem1 4614  uzwo3lem2 4615  expaddt 4698  znnenlem 4929  infmap2lem1 4951  ocsh 5164  ococss 5174  occllem6 5185  projlem13 5205  projlem26 5218  projlem28 5220  pjoml 5271  chintcl 5296  shmods 5363  spansnsst 5476  elspansn4t 5478  h1datom 5483  5oalem6 5549  atom1d 5750  atcvat2 5772  atcvat3 5774  atcvat4 5775  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdi 5785  sumdmdlem 5786

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