Theorem exp4c 380

Description: An exportation inference.

Hypothesis

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

Assertion

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

Proof of Theorem exp4c

Step	Hyp	Ref	Expression
1		exp4c.1	. . 3 |- (ph -> (((ps /\ ch) /\ th) -> ta))
2	1	exp3a 375	. 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:  tfrlem1 3911  oawordri 4184  oaordex 4192  odi 4210  pssnn 4534  aceq6b 4742  alephval3 4903  prlem934 5139  prlem936b 5154  seq1rn2 6321  seqzrn2 6556  expmwordit 6606  tgss2t 7637  metelcls 7965  atcvatlem 10312

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