Theorem exp4b 365

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 364	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  370  reuss2  3402  nndi  6454  mulnqprl  7509  mulnqpru  7510  distrlem5prl  7527  distrlem5pru  7528  recexprlemss1l  7576  recexprlemss1u  7577  lemul12a  8757  nnmulcl  8878  elfz0fzfz0  10061  fzo1fzo0n0  10118  fzofzim  10123  elfzodifsumelfzo  10136  le2sq2  10530  oddprmgt2  12066  infpnlem1  12289