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 4434  sdomen2 4482  fodomr 4483  mapenlem2 4490  xpmapenlem4 4499  sucdomi 4524  domfiOLD 4539  unblem1 4540  unblem2 4541  fiint 4559  fiintOLD 4560  supnub 4582  inf3lem2 4614  inf3lem3 4615  inf3lem6 4618  unbnnt 4639  zfregs 4647  r1ord 4655  karden 4726  aceq5lem5 4739  aceq5 4740  aceq6b 4742  kmlem1 4765  kmlem9 4773  numthlem 4783  zorn2lem7 4794  sucdom 4842  indpi 5034  genpnmax 5110  ltaddpr 5140  ltexprlem7 5148  ltaprlem 5150  prlem936b 5154  prlem936 5155  suplem1pr 5161  ssgt0sr 5217  addsubt 5384  lelttrt 5523  ltletrt 5524  letrt 5525  xrlelttrt 5562  xrltletrt 5563  xrletrt 5564  nnleltp1t 5954  bndndx 6073  xrsupsslem 6076  xrinfmsslem 6077  supxrun 6085  elnnz1 6155  uzwo4OLD 6210  btwnz 6215  uzwo3lem1 6216  uzwo3lem2 6217  iooss1 6373  iooss2 6374  icounlem 6412  ioojoint 6416  uzwo 6455  uzwoOLD 6456  expgt0t 6589  expgt1t 6592  mulexpt 6594  recexpt 6595  expaddt 6596  expmult 6597  expword2it 6605  bernneq 6652  cau2 6913  cau5i 6917  cvg2 6922  cvg3 6923  bcclt 6972  fsumsplit 7020  climconst3 7096  climserzle 7147  caucvglem2 7158  caucvglem4 7160  caucvg 7163  cvgratlem2 7251  abscncflem 7274  infmap2lem1 7579  basis2t 7615  tgss2t 7637  0ntr 7702  cncnp 7778  metxp 7834  bl2in 7843  ssbl 7855  opnin 7869  metcnp4lem2 7969  xplmi 7973  xplm 7975  iscms2lem4 7992  bcthlem1 7999  bcthlem20 8018  bcthlem29 8027  grpidinvlem3 8050  grpinveu 8064  ubthlem13 8541  ubthlem14 8542  efifolem4 8725  ocsh 9156  ococss 9166  ocnelt 9170  projlem13 9198  projlem26 9211  projlem28 9213  shmods 9362  spansnsst 9494  h1datom 9504  5oalem6 9604  hoaddsubt 9742  homco2t 9901  lnopcon 9963  lnfncon 9990  adjmult 10025  atom1d 10280  chjatom 10284  atoml 10309  atcvat2 10314  atcvat3 10323  atcvat4 10324  mdsymlem3 10332  mdsymlem5 10334  mdsymlem6 10335  sumdmdi 10342  sumdmdlem 10345  sumdmdlem2 10346  cdj3lem2a 10363  cdj3lem3a 10366  elioo1t3 10496  hmeogrp 10538  homcard 10539  qusp 10555  fgsb2 10580  iintlem1 10632

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