Theorem exp4b 364

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

Hypothesis

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

Assertion

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

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 |- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
2	1	ex 114	. 2 |- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )
3	2	exp4a 363	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exp43  369  reuss2  3351  nndi  6375  mulnqprl  7369  mulnqpru  7370  distrlem5prl  7387  distrlem5pru  7388  recexprlemss1l  7436  recexprlemss1u  7437  lemul12a  8613  nnmulcl  8734  elfz0fzfz0  9896  fzo1fzo0n0  9953  fzofzim  9958  elfzodifsumelfzo  9971  le2sq2  10361  oddprmgt2  11803