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 3886  oelim 4153  en3d 4382  zorn2lem7 4766  divexpt 6530  infxpidmlem11 7505  basgen2t 7581  neibl 7817  bcthlem28 7960  blocnilem 8395  ipblnfi 8447  shscl 9196  spanun 9382

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