Theorem exp4b 367

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exp43  372  reuss2  3485  nndi  6649  mulnqprl  7778  mulnqpru  7779  distrlem5prl  7796  distrlem5pru  7797  recexprlemss1l  7845  recexprlemss1u  7846  lemul12a  9032  nnmulcl  9154  elfz0fzfz0  10351  fzo1fzo0n0  10412  fzofzim  10417  elincfzoext  10428  elfzodifsumelfzo  10436  le2sq2  10867  swrdswrd  11276  swrdccat3blem  11310  oddprmgt2  12696  infpnlem1  12922  lmodvsdi  14315