Theorem 3expib 1230

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3expib	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1226	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 254	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002

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  df-3an 1004

This theorem is referenced by:  3anidm12  1329  mob  2985  eqbrrdva  4891  funimaexglem  5403  fco  5488  f1oiso2  5950  caovimo  6198  smoel2  6447  nnaword  6655  3ecoptocl  6769  rex2dom  6969  sbthlemi10  7129  distrnq0  7642  addassnq0  7645  prcdnql  7667  prcunqu  7668  genpdisj  7706  cauappcvgprlemrnd  7833  caucvgprlemrnd  7856  caucvgprprlemrnd  7884  nn0n0n1ge2b  9522  fzind  9558  icoshft  10182  fzen  10235  seq3coll  11059  shftuz  11323  mulgcd  12532  algcvga  12568  lcmneg  12591  isnmgm  13388  gsummgmpropd  13422  issgrpd  13440  iscmnd  13830  unitmulclb  14072  rmodislmodlem  14308  rmodislmod  14309  blssps  15095  blss  15096  metcnp3  15179  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  iswlkg  16032