Theorem exp42 385

Description: An exportation inference.

Hypothesis

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

Assertion

Ref	Expression
exp42	|- (ph -> (ps -> (ch -> (th -> ta))))

Proof of Theorem exp42

Step	Hyp	Ref	Expression
1		exp42.1	. . 3 |- (((ph /\ (ps /\ ch)) /\ th) -> ta)
2	1	exp31 378	. 2 |- (ph -> ((ps /\ ch) -> (th -> ta)))
3	2	exp3a 376	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  isofrlem 3908  oelim 4176  en3d 4408  zorn2lem7 4811  divexpt 6607  infxpidmlem11 7570  basgen2t 7645  neibl 7881  bcthlem28 8030  blocnilem 8467  ipblnfi 8519  shscl 9283  spanun 9469

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