Theorem imp3a 279

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  imp32 281  imp4c 284  imp4d 285  adantld 307  imdistan 339  syland 352  dedlemb 570  sbied 903  ra42 1245  r19.23ad 1285  r19.23adv 1286  vtocl3ga 1389  rcla42v 1404  prel12 1875  euuni 1954  trel 2048  sotrieq 2149  suplub 2161  supnub 2162  wefrc 2195  tz7.7 2224  ordtr2 2257  oneqmini 2272  onmindif2 2313  peano5 2394  tfindsg2 2403  funssres 2698  fv3 2839  fvelrn 2883  fopab2 2891  funfvima 2904  cbvfo 2923  isomin 2937  isofrlem 2939  f1oweOLD 2944  tfr3 2964  tz7.48-1 2994  tz7.48-2 2995  tz7.49 2997  tz7.49c 2998  omordi 3164  oen0 3165  nndi 3180  nnmass 3181  nnmordi 3188  3ecoptocl 3241  th3qlem1 3250  unen 3338  ensdomtr 3372  sdomen2 3380  ssenen 3399  pssnn 3428  unblem1 3431  isfinite2 3437  fiint 3445  inf3lem2 3465  zfregs 3491  aceq6b 3565  zornlem7 3609  fodom 3613  unxpdomlem 3649  ondomon 3662  alephord2i 3682  cardinfima 3696  indpi 3828  ltexpq 3874  ltrpq 3879  genpss 3901  genpnmax 3904  distrlem1pr 3921  distrlem5pr 3925  1idpr 3927  prlem934a 3931  ltaddpr 3934  ltexprlem1 3936  ltexprlem6 3941  prlem936b 3948  prlem936 3949  reclem4pr 3953  suplem1pr 3955  mulcmpblnr 3977  recexsrlem 4006  recexsr 4010  axnegex 4078  ltlent 4288  lelttrt 4289  ltletrt 4290  letrt 4291  nnleltp1t 4448  sup2 4510  creur 4532  creui 4533  zltp1let 4597  uzwo 4605  nnwoOLD 4608  sqr2irrlem3 4779  znnenlem 4929  chcompl 5150  ocin 5177  occllem6 5185  projlem26 5218  pjthu 5241  pjthu2 5242  shmods 5363  spansneleq 5475  elspansn3t 5477  elspansn5t 5479  spansncv 5542  stjt 5676  atom1d 5750  atcvat2 5772  mdsymlem3 5778  mdsymlem6 5781  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org