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 3906  oawordri 4177  oaordex 4185  odi 4203  pssnn 4522  aceq6b 4725  alephval3 4886  prlem934 5122  prlem936b 5137  seq1rn2 6271  seqzrn2 6501  expmwordit 6551  tgss2t 7597  metelcls 7927  atcvatlem 10268

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