Theorem expdimp 377

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 376	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp 350	1 |- ((ph /\ ps) -> (ch -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  r19.23advv 1752  reu3 1934  ordsseleq 2982  ordtr2 3008  oneqmini 3023  omsmo 4263  fodomr 4489  isfinite2 4557  supnub 4591  inf3lem6 4627  zorn2lem7 4804  sucdom 4852  sucdomOLD 4853  letrt 5537  xrletrt 5576  supxrun 6087  uzwo4OLD 6212  icounlem 6413  cau5i 6917  cvg3 6923  infmap2lem1 7581  tgss2t 7636  cncnp 7775  metxp 7831  opnin 7866  xplmi 7970  xplm 7972  atcvat3 10318  sumdmdlem2 10341  hmeogrp 10524  sfseqeq 10529  qusp 10541

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