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 697  mpan2i 698  mpand 700  mpan2d 701  pclem6 740  pm5.75 748  3impib 830  ax11indn 1366  mopick 1433  r19.21aivv 1719  r19.23advv 1748  reu3 1929  reupick 2277  trel 2684  pwssun 2824  reuuni1 2879  elpwunsn 2909  wefrc 2940  ordelord 2967  tz7.7 2970  ordsseleq 2973  ordtr2 2999  oneqmini 3014  trsuc 3052  limuni3 3120  ordom 3138  weinxp 3230  ssrel 3244  relop 3272  funcnvuni 3561  fnun 3591  fconst5 3845  funfvima 3849  f1oweALT 3903  tfrlem5 3912  tz7.48lem 3952  tz7.49 3956  abianfp 3959  elrnoprabg 4121  oecl 4169  oaordex 4189  oaass 4192  oarec 4193  omwordri 4200  odi 4207  omass 4208  oen0 4210  oeordi 4211  oewordri 4216  oeworde 4217  nnarcl 4229  omsmolem 4253  omsmo 4254  unen 4427  sdomen2 4475  fodomr 4476  mapenlem2 4483  xpmapenlem4 4492  sucdomi 4516  domfi 4529  unblem1 4530  unblem2 4531  fiint 4547  supnub 4569  inf3lem2 4601  inf3lem3 4602  inf3lem6 4605  unbnnt 4626  zfregs 4634  r1ord 4642  karden 4713  aceq5lem5 4726  aceq5 4727  aceq6b 4729  kmlem1 4752  kmlem9 4760  numthlem 4770  zorn2lem7 4781  sucdom 4829  indpi 5021  genpnmax 5097  ltaddpr 5127  ltexprlem7 5135  ltaprlem 5137  prlem936b 5141  prlem936 5142  suplem1pr 5148  ssgt0sr 5204  addsubt 5371  lelttrt 5510  ltletrt 5511  letrt 5512  xrlelttrt 5549  xrltletrt 5550  xrletrt 5551  nnleltp1t 5915  bndndx 6034  xrsupsslem 6037  xrinfmsslem 6038  supxrun 6046  elnnz1 6116  uzwo4OLD 6172  btwnz 6177  uzwo3lem1 6178  uzwo3lem2 6179  iooss1 6328  iooss2 6329  icounlem 6363  uzwo 6405  uzwoOLD 6406  expgt0t 6539  expgt1t 6542  mulexpt 6544  recexpt 6545  expaddt 6546  expmult 6547  expword2it 6555  bernneq 6602  cau2 6879  cau5i 6883  cvg2 6888  cvg3 6889  bcclt 6940  fsumsplit 6988  climconst3 7064  climserzle 7116  caucvglem2 7127  caucvglem4 7129  caucvg 7132  cvgratlem2 7222  abscncflem 7245  znnenlemOLD 7480  infmap2lem1 7558  basis2t 7594  tgss2t 7616  0ntr 7681  cncnp 7757  metxp 7815  bl2in 7825  ssbl 7838  opnin 7852  metcnp4lem2 7952  xplmi 7956  xplm 7958  iscms2lem4 7975  bcthlem1 7982  bcthlem20 8001  bcthlem29 8010  grpidinvlem3 8033  grpinveu 8047  ubthlem13 8525  ubthlem14 8526  efifolem4 8704  ocsh 9144  ococss 9154  ocnelt 9158  projlem13 9186  projlem26 9199  projlem28 9201  shmods 9350  spansnsst 9484  h1datom 9494  5oalem6 9595  hoaddsubt 9733  homco2t 9892  lnopcon 9954  lnfncon 9981  adjmult 10016  atom1d 10271  chjatom 10275  atoml 10300  atcvat2 10305  atcvat3 10314  atcvat4 10315  mdsymlem3 10323  mdsymlem5 10325  mdsymlem6 10326  sumdmdi 10333  sumdmdlem 10336  sumdmdlem2 10337  cdj3lem2a 10354  cdj3lem3a 10357  elioo1t3 10477  hmeogrp 10519  homcard 10520  qusp 10524  fgsb2 10543  iintlem1 10583

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