Theorem exp42 383

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  isofrlem 3898  oelim 4166  en3d 4395  zorn2lem7 4781  divexpt 6549  infxpidmlem11 7541  basgen2t 7618  neibl 7860  bcthlem28 8009  blocnilem 8448  ipblnfi 8500  shscl 9269  spanun 9455

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