Theorem exp4b 359

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  exp43  364  reuss2  3244  nndi  6088  mulnqprl  6758  mulnqpru  6759  distrlem5prl  6776  distrlem5pru  6777  recexprlemss1l  6825  recexprlemss1u  6826  lemul12a  7940  nnmulcl  8060  elfz0fzfz0  9137  fzo1fzo0n0  9192  fzofzim  9197  elfzodifsumelfzo  9210  le2sq2  9551  oddprmgt2  10515