Theorem expimpd 382

Description: Exportation followed by a deduction version of importation.

Hypothesis

Ref	Expression
expimpd.1	|- ((ph /\ ps) -> (ch -> th))

Assertion

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

Proof of Theorem expimpd

Step	Hyp	Ref	Expression
1		expimpd.1	. . 3 |- ((ph /\ ps) -> (ch -> th))
2	1	ex 380	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp3a 368	1 |- (ph -> ((ps /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  sotrieq 2917  oneqmini 3074  onmindif2 3118  isofrlem 3959  tz7.48-2 4015  th3qlem1 4375  ensdomtr 4534  pssnn 4599  fodomfib 4627  supnub 4642  zfregs 4709  aceq6b 4804  unidom 4870  alephord2i 4942  cardinfima 4956  alephval2 4967  distrlem5pr 5196  1idpr 5198  suplem1pr 5226  letr 5590  xrletr 5629  sup2 6133  zltp1le 6263  flval3 6351  elioc2 6415  elico2 6416  elicc2 6417  creur 6832  cau4ii 7008  cau5i 7009  clim2serz 7224  caucvglem4 7250  cvgratlem2 7341  infpnlem1 7598  subtop 7733  neindisj 7816  sncld 7872  bl2in 7928  metcnp 7972  metcnss 7983  lmuni 8036  lmle 8045  iscms2lem4 8077  lmcau 8081  bcthlem16 8099  bcthlem17 8100  occllem6 9261  pjtheui 9318  spansncvi 9680  cnlnssadj 10096  leopmuli 10149  mdsl0 10321  sumdmdii 10426  cdrci 10588  cmphmp 10615  hmphsyma 10622

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 154  df-an 232

Copyright terms: Public domain