Theorem exp4d 383

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  tfrlem9 3925  omass 4217  pssnn 4544  rankr1 4684  cardinfima 4902  ltaddpr 5152  ltexprlem7 5160  prlem936b 5166  prlem936 5167  facdivt 6942  cvgratlem1ALT 7247  cvgratlem1 7250  infpnlem1 7507  lmcau 7993  ubthlem13 8537  nmcopexlem6 9951  nmcfnexlem6 9980  atcvatlem 10307  mdsymlem5 10329  mdsymlem7 10331

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