Theorem expimpd 404

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 402	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp3a 388	1 |- (ph -> ((ps /\ ch) -> th))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sotrieqOLD 3617  oneqmini 3714  onmindif2 3893  isofrlem 4878  tz7.48-2 5166  th3qlem1 5373  ensdomtr 5534  pssnn 5628  fodomfib 5657  supnub 5672  zfregs 5754  aceq6b 5904  unidom 5970  alephord2i 6025  cardinfima 6039  alephval2 6050  distrlem5pr 6283  1idpr 6285  suplem1pr 6313  letr 6695  xrletr 6739  sup2 7260  zltp1le 7390  flval3 7479  elioc2 7558  elico2 7559  elicc2 7560  creur 7992  cau4ii 8170  cau5i 8171  clim2serz 8394  caucvglem4 8420  cvgratlem2 8513  infpnlem1 8775  subtop 8916  neindisj 9007  sncld 9064  bl2in 9120  metcnp 9165  metcnss 9176  lmuni 9229  lmle 9238  iscms2lem4 9270  lmcau 9274  bcthlem16 9292  bcthlem17 9293  elpreima 10161  cdrci 10182  uptx 10226  subcld 10254  filrn 10293  elfilmap2 10313  elfilmap3 10314  occllem6 10811  pjtheui 10868  spansncvi 11232  cnlnssadj 11650  leopmuli 11704  mdsl0 11882  sumdmdii 11987  bnj594 13300  frxp 13951  wfr3g 13956  frr3g 13980  sltval2 13997  cmphmp 14878  hmphsyma 14882  cnsubsp2 15427  2ndc1stc 15477  fnejoin2 15531  filfinnfr 15561  filufint 15574  unirep 15664  difxp 15690  frfi 15771  sdclem2 15810  blhalf 15846  haustlmu 15906  lmtlm 15908  txsubsp 15912  txmet 15925  sstotbnd 15936  totbndss 15937  ismtyhmeolem 15950  heiborlem1 15955  heiborlem23 15977  heiborlem29 15983  heiborlem32 15986  heiborlem37 15991  pcohtpylem3 16082  ordpss 16428  pltnle 16786  pltletr 16791  paddasslem14 17294  paddasslem15 17295  paddasslem16 17296  pmapjoin 17313

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 164  df-an 242

Copyright terms: Public domain