Theorem expdimp 375

Description: A deduction version of exportation, followed by importation.

Hypothesis

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

Assertion

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

Proof of Theorem expdimp

Step	Hyp	Ref	Expression
1		exp3a.1	. . 3 |- (ph -> ((ps /\ ch) -> th))
2	1	exp3a 374	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp 348	1 |- ((ph /\ ps) -> (ch -> th))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  r19.23advv 1787  reu3 1969  ordsseleq 3031  ordtr2 3057  oneqmini 3072  omsmo 4341  fodomr 4570  isfinite2 4633  supnub 4666  inf3lem6 4704  zorn2lem7 4880  sucdom 4931  letr 5614  xrletr 5653  supxrun 6195  uzwo4OLD 6323  icounlem 6472  cau5ii 7040  cvg3i 7046  infmap2lem1 7704  tgss2 7761  indistop 7770  cncnp 7898  metxp 7954  opnin 7989  xplmi 8093  xplm 8095  atcvat3i 10441  sumdmdlem2 10464  hmeogrp 10674  sfseqeq 10679  qusp 10694

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 145  df-an 223

Copyright terms: Public domain