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 1194  equs5 1220  a12study 1377  a12studyALT 1378  ra42 1694  r19.23ad 1743  reu3 1928  sbciegft 1956  uniiunlem 2129  prel12 2481  opthpr 2482  trel 2683  sotrieq 2857  elpwunsn 2908  wefrc 2939  tz7.7 2969  ordtr2 2998  oneqmini 3013  onmindif2 3057  peano5 3149  tfindsg2 3159  relop 3271  funssres 3548  fv3 3728  fopab2 3818  funfvima 3847  cbvfo 3880  isomin 3894  isofrlem 3896  f1oweALT 3901  tfrlem2 3907  tfr3 3921  tz7.48-1 3951  tz7.48-2 3952  tz7.49c 3955  omordi 4190  odi 4203  omass 4204  oen0 4206  oeordi 4207  nnmordi 4239  th3qlem1 4307  unen 4423  ensdomtr 4460  sdomen2 4471  ssenen 4493  pssnn 4522  domfi 4525  isfinite2 4532  unifi 4541  fiint 4543  fodomfib 4550  suplub 4564  supnub 4565  inf3lem2 4597  zfregs 4630  aceq6b 4725  zorn2lem7 4777  fodom 4781  brdom6disj 4788  unidom 4791  unxpdomlem 4826  ondomon 4839  alephord2i 4860  cardinfima 4874  alephval2 4885  indpi 5017  ltexpq 5063  ltrpq 5068  genpss 5090  genpnmax 5093  distrlem1pr 5110  distrlem5pr 5114  1idpr 5116  prlem934a 5120  ltaddpr 5123  ltexprlem1 5125  ltexprlem6 5130  prlem936b 5137  prlem936 5138  reclem4pr 5142  suplem1pr 5144  mulcmpblnr 5166  recexsrlem 5195  recexsr 5199  ltlent 5505  lelttrt 5506  ltletrt 5507  letrt 5508  xrlelttrt 5545  xrltletrt 5546  xrletrt 5547  mulgt1t 5811  nnleltp1t 5911  sup2 6008  supxrre 6040  zltp1let 6138  uzwo4OLD 6168  flval3t 6195  ser1add2 6288  ser1add 6289  elioc2t 6335  elico2t 6336  elicc2t 6337  uzwo 6400  uzwoOLD 6401  fsequb 6468  expgt0t 6534  expgt1t 6537  recexpt 6540  expword2it 6550  bernneq 6597  sqr2irrlem3 6671  creur 6688  creui 6689  cau4i 6870  cau5 6871  fsumcom 6981  fsumrev 6982  clim2serzt 7087  iserzmulc1 7089  caucvglem4 7113  cvgratlem1ALT 7199  cvgratlem1 7202  cvgratlem2 7203  abscncflem 7226  ivthlem7 7239  ivthlem7OLD 7248  acdc2 7449  acdc 7454  znnenlemOLD 7461  infpnlem1 7466  subtop 7606  clsval2 7645  neindisj 7691  sncld 7747  bl2in 7805  rnblssm 7813  metcnp 7849  metcnss 7860  lmuni 7913  lmle 7922  xpcn 7938  iscms2lem4 7954  lmcau 7958  bcthlem16 7976  bcthlem17 7977  bcthlem26 7986  grplactf1o 8061  ipblnfi 8475  ubthlem13 8500  spwmo 8613  ocin 9124  occllem6 9133  projlem26 9166  pjtheu 9190  shmods 9317  spansneleq 9449  spansneleqOLD 9450  spansncv 9554  nlelch 9950  cnlnssadj 9969  leopmulit 10022  pjnmop 10031  stjt 10118  mdsl0 10193  atom1d 10236  atcvat2 10270  irredlem1 10273  irred 10277  mdsymlem3 10288  mdsymlem6 10291  sumdmdi 10298  uninqs 10400  cdrci 10440  cmphmp 10467  hmphsyma 10474  hmphtr 10477  homcard 10485  qusp 10489

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