Theorem exp4d 298

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  tfrlem9 2957  tz7.49 2997  pssnn 3428  rankr1 3518  cardinfima 3696  ltaddpr 3934  ltexprlem7 3942  prlem936b 3948  prlem936 3949  seqrn 4673  atcvatlem 5770  mdsymlem5 5780  mdsymlem7 5782

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org