Theorem imp3a 361

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp32 363  imp4c 366  imp4d 367  adantld 390  imdistan 442  syland 457  dedlemb 762  3expib 835  sbied 1193  equs5 1219  a12study 1376  a12studyALT 1377  ra42 1693  r19.23ad 1742  reu3 1927  sbciegft 1955  uniiunlem 2128  prel12 2480  opthpr 2481  trel 2682  sotrieq 2856  elpwunsn 2907  wefrc 2938  tz7.7 2968  ordtr2 2997  oneqmini 3012  onmindif2 3056  peano5 3148  tfindsg2 3158  relop 3270  funssres 3544  fv3 3724  fopab2 3814  funfvima 3843  cbvfo 3876  isomin 3890  isofrlem 3892  f1oweALT 3897  tfrlem2 3903  tfr3 3917  tz7.48-1 3947  tz7.48-2 3948  tz7.49c 3951  omordi 4187  odi 4200  omass 4201  oen0 4203  oeordi 4204  nnmordi 4236  th3qlem1 4304  unen 4420  ensdomtr 4457  sdomen2 4468  ssenen 4490  pssnn 4519  domfi 4522  isfinite2 4529  unifi 4538  fiint 4540  fodomfib 4547  suplub 4561  supnub 4562  inf3lem2 4594  zfregs 4627  aceq6b 4722  zorn2lem7 4774  fodom 4778  brdom6disj 4785  unidom 4788  unxpdomlem 4823  ondomon 4836  alephord2i 4857  cardinfima 4871  alephval2 4882  indpi 5014  ltexpq 5060  ltrpq 5065  genpss 5087  genpnmax 5090  distrlem1pr 5107  distrlem5pr 5111  1idpr 5113  prlem934a 5117  ltaddpr 5120  ltexprlem1 5122  ltexprlem6 5127  prlem936b 5134  prlem936 5135  reclem4pr 5139  suplem1pr 5141  mulcmpblnr 5163  recexsrlem 5192  recexsr 5196  ltlent 5503  lelttrt 5504  ltletrt 5505  letrt 5506  xrlelttrt 5543  xrltletrt 5544  xrletrt 5545  mulgt1t 5809  nnleltp1t 5909  sup2 6006  supxrre 6038  zltp1let 6136  uzwo4OLD 6166  flval3t 6190  ser1add2 6283  ser1add 6284  elioc2t 6330  elico2t 6331  elicc2t 6332  uzwo 6395  uzwoOLD 6396  fsequb 6463  expgt0t 6528  expgt1t 6531  recexpt 6534  expword2it 6544  bernneq 6591  sqr2irrlem3 6664  creur 6681  creui 6682  cau4i 6863  cau5 6864  fsumcom 6974  fsumrev 6975  clim2serzt 7078  iserzmulc1 7080  caucvglem4 7104  cvgratlem1ALT 7190  cvgratlem1 7193  cvgratlem2 7194  abscncflem 7217  ivthlem7 7230  ivthlem7OLD 7239  acdc2 7440  acdc 7445  znnenlemOLD 7452  infpnlem1 7457  subtop 7596  clsval2 7635  neindisj 7681  sncld 7737  bl2in 7795  rnblssm 7803  metcnp 7839  metcnss 7850  lmuni 7902  lmle 7911  xpcn 7926  iscms2lem4 7942  lmcau 7946  bcthlem16 7964  bcthlem17 7965  bcthlem26 7974  grplactf1o 8049  ipblnfi 8460  ubthlem13 8485  spwmo 8598  ocin 9108  occllem6 9117  projlem26 9150  pjtheu 9173  shmods 9300  spansneleq 9432  spansneleqOLD 9433  spansncv 9537  nlelch 9932  cnlnssadj 9951  leopmulit 10004  pjnmop 10013  stjt 10100  mdsl0 10174  atom1d 10217  atcvat2 10251  irredlem1 10254  irred 10258  mdsymlem3 10269  mdsymlem6 10272  sumdmdi 10278  uninqs 10378  cdrci 10417  cmphmp 10444  hmphsyma 10451  hmphtr 10454  homcard 10462  qusp 10466

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