Theorem exp4d 381

Description: An exportation inference.

Hypothesis

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

Assertion

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

Proof of Theorem exp4d

Step	Hyp	Ref	Expression
1		exp4d.1	. . 3 |- (ph -> ((ps /\ (ch /\ th)) -> ta))
2	1	exp3a 375	. 2 |- (ph -> (ps -> ((ch /\ th) -> ta)))
3	2	exp4a 378	1 |- (ph -> (ps -> (ch -> (th -> ta))))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  tfrlem9 3919  omass 4211  pssnn 4534  rankr1 4674  cardinfima 4891  ltaddpr 5140  ltexprlem7 5148  prlem936b 5154  prlem936 5155  facdivt 6942  cvgratlem1ALT 7247  cvgratlem1 7250  infpnlem1 7506  lmcau 7996  ubthlem13 8541  spwpr3OLD 8662  nmcopexlem6 9956  nmcfnexlem6 9985  atcvatlem 10312  mdsymlem5 10334  mdsymlem7 10336

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