Theorem exp3a 375

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 347	. 2 |- (((ps /\ ch) -> th) <-> (ps -> (ch -> th)))
3	1, 2	sylib 198	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  exp32 377  exp4b 379  exp4c 380  exp4d 381  exp42 383  exp44 385  imdistan 442  syland 457  anabsi7 497  mpani 698  mpan2i 699  mpand 701  mpan2d 702  pclem6 741  pm5.75 749  3impib 831  ax11indn 1366  mopick 1433  r19.21aivv 1720  r19.23advv 1749  reu3 1931  reupick 2279  trel 2687  pwssun 2827  reuuni1 2882  elpwunsn 2912  wefrc 2943  ordelord 2970  tz7.7 2973  ordsseleq 2976  ordtr2 3002  oneqmini 3017  trsuc 3055  limuni3 3123  ordom 3141  weinxp 3233  ssrel 3247  relop 3275  funcnvuni 3564  fnun 3594  fconst5 3848  funfvima 3852  f1oweALT 3906  tfrlem5 3915  tz7.48lem 3955  tz7.49 3959  abianfp 3962  elrnoprabg 4124  oecl 4172  oaordex 4192  oaass 4195  oarec 4196  omwordri 4203  odi 4210  omass 4211  oen0 4213  oeordi 4214  oewordri 4219  oeworde 4220  nnarcl 4232  omsmolem 4256  omsmo 4257  unen 4432  sdomen2 4480  fodomr 4481  mapenlem2 4488  xpmapenlem4 4497  sucdomi 4521  domfi 4534  unblem1 4535  unblem2 4536  fiint 4552  supnub 4574  inf3lem2 4606  inf3lem3 4607  inf3lem6 4610  unbnnt 4631  zfregs 4639  r1ord 4647  karden 4718  aceq5lem5 4731  aceq5 4732  aceq6b 4734  kmlem1 4757  kmlem9 4765  numthlem 4775  zorn2lem7 4786  sucdom 4834  indpi 5026  genpnmax 5102  ltaddpr 5132  ltexprlem7 5140  ltaprlem 5142  prlem936b 5146  prlem936 5147  suplem1pr 5153  ssgt0sr 5209  addsubt 5376  lelttrt 5515  ltletrt 5516  letrt 5517  xrlelttrt 5554  xrltletrt 5555  xrletrt 5556  nnleltp1t 5942  bndndx 6061  xrsupsslem 6064  xrinfmsslem 6065  supxrun 6073  elnnz1 6143  uzwo4OLD 6198  btwnz 6203  uzwo3lem1 6204  uzwo3lem2 6205  iooss1 6359  iooss2 6360  icounlem 6398  ioojoint 6402  uzwo 6441  uzwoOLD 6442  expgt0t 6575  expgt1t 6578  mulexpt 6580  recexpt 6581  expaddt 6582  expmult 6583  expword2it 6591  bernneq 6638  cau2 6898  cau5i 6902  cvg2 6907  cvg3 6908  bcclt 6957  fsumsplit 7005  climconst3 7081  climserzle 7132  caucvglem2 7143  caucvglem4 7145  caucvg 7148  cvgratlem2 7236  abscncflem 7259  infmap2lem1 7564  basis2t 7600  tgss2t 7622  0ntr 7687  cncnp 7763  metxp 7819  bl2in 7828  ssbl 7840  opnin 7854  metcnp4lem2 7954  xplmi 7958  xplm 7960  iscms2lem4 7977  bcthlem1 7984  bcthlem20 8003  bcthlem29 8012  grpidinvlem3 8035  grpinveu 8049  ubthlem13 8526  ubthlem14 8527  efifolem4 8710  ocsh 9141  ococss 9151  ocnelt 9155  projlem13 9183  projlem26 9196  projlem28 9198  shmods 9347  spansnsst 9479  h1datom 9489  5oalem6 9589  hoaddsubt 9727  homco2t 9886  lnopcon 9948  lnfncon 9975  adjmult 10010  atom1d 10265  chjatom 10269  atoml 10294  atcvat2 10299  atcvat3 10308  atcvat4 10309  mdsymlem3 10317  mdsymlem5 10319  mdsymlem6 10320  sumdmdi 10327  sumdmdlem 10330  sumdmdlem2 10331  cdj3lem2a 10348  cdj3lem3a 10351  elioo1t3 10468  hmeogrp 10510  homcard 10511  qusp 10515  fgsb2 10535  iintlem1 10575

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