Theorem imp3a 359

Description: Importation deduction.

Hypothesis

Ref	Expression
imp3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
imp3a	|- (ph -> ((ps /\ ch) -> th))

Proof of Theorem imp3a

Step	Hyp	Ref	Expression
1		imp3.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		impexp 345	. 2 |- (((ps /\ ch) -> th) <-> (ps -> (ch -> th)))
3	1, 2	sylibr 198	1 |- (ph -> ((ps /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  imp32 361  imp4c 364  imp4d 365  expimpd 373  adantld 390  imdistan 444  syland 459  dedlemb 768  dn1 779  3expib 842  sbied 1232  equs5 1258  a12study 1417  a12studyALT 1418  ra42 1742  r19.23ad 1791  reu3 1977  sbciegft 2007  uniiunlem 2184  prel12 2549  opthpr 2550  trel 2761  wefrc 2970  tz7.7 3001  ordtr2 3019  elpwunsn 3135  tfindsg2 3214  peano5 3241  relop 3365  funssres 3657  fv3 3844  fopab2 3937  funfvima 3966  cbvfo 3999  isomin 4013  f1oweALT 4020  tfrlem2 4213  tfr3 4227  tz7.48-1 4257  tz7.49c 4261  omordi 4333  odi 4346  omass 4347  oen0 4349  oeordi 4350  nnmordi 4386  unen 4575  sdomen2 4627  ssenen 4651  pssnn 4681  domfi 4684  isfinite2 4692  unifi 4701  fiint 4703  suplub 4724  inf3lem2 4759  zfregs 4793  aceq6b 4888  zorn2lem7 4940  fodom 4944  brdom6disj 4951  unxpdomlem 4993  ondomon 5006  indpi 5188  ltexpq 5234  ltrpq 5239  genpss 5261  genpnmax 5264  distrlem1pr 5281  1idpr 5287  prlem934a 5291  ltaddpr 5294  ltexprlem1 5296  ltexprlem6 5301  prlem936b 5308  prlem936 5309  reclem4pr 5313  mulcmpblnr 5337  recexsrlem 5366  recexsr 5370  ltlen 5676  lelttr 5677  ltletr 5678  xrlelttr 5716  xrltletr 5717  mulgt1 5989  nnleltp1 6100  supxrre 6251  zltp1le 6349  uzwo4OLD 6381  uzwo 6582  uzwoOLD 6583  fzen 6622  fsequb 6654  ser1add2i 6703  ser1addi 6704  expgt0 6783  expgt1 6786  exprec 6789  exprecOLD 6790  expword2i 6802  bernneq 6849  bernneqOLD 6850  sqr2irrlem3 6927  creui 6944  fsumcom 7231  fsumrev 7232  iserzmulc1 7339  cvgratlem1ALT 7452  cvgratlem1 7455  abscncflem 7479  ivthlem7 7492  acdc2 7702  acdc 7707  infpnlem1 7718  clsval2 7895  rnblssm 8061  xpcn 8187  bcthlem26 8235  gxnn0add 8330  gxadd 8331  gxnn0mul 8333  gxmul 8334  grplactf1o 8339  ipblnfi 8772  ubthlem13 8800  ubthlem13OLD 8801  spwmo 8918  ocin 9445  occllem6 9454  projlem26 9487  shmodsi 9638  spansneleq 9769  nlelchi 10273  pjnmopi 10355  stj 10443  atom1d 10561  atcvat2i 10596  irredlem1 10599  irredi 10603  mdsymlem3 10614  mdsymlem6 10617  uninqs 10730  hmphtr 11037  homcard 11045  qusp 11068  limfillem2 11102  imp5d 11343  expl 11360  trer 11409  finminlem 11418  finsschain 11425  ordtypelem7 11433  hartog 11436  elomsubsd 11446  omsublim 11448  opncldf1 11454  hausnei2 11471  compsublem 11487  hscptsscld 11491  alexsublem2 11497  alexsublem4 11499  alexsub 11500  subtopmet 11506  2ndcctbss 11539  fnessref 11564  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  fnemeet1 11589  fnemeet2 11590  fnejoin2 11592  t1t0 11608  isnrm2 11613  fgid 11637  fgfil 11638  fgmin 11639  fbfgss 11640  extbas1 11641  isufil2 11650  filssufillem 11655  filssufil 11656  ufileulem 11657  ufileu 11658  filufint 11659  filcon 11665  flimopn 11679  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  fcluscf 11724  flimfnfcls 11727  fcluscnp 11730  filnetlem4 11766  filnetlem5 11767  dif1en 11833  fimax 11837  sdc 11877  txbas 11973  heiborlem35 12045

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 145  df-an 223

Copyright terms: Public domain