Theorem 3expib 1233

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 1229	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 254	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

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

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 1007

This theorem is referenced by:  3anidm12  1332  mob  3002  eqbrrdva  4930  funimaexglem  5444  fco  5532  f1oiso2  6006  caovimo  6256  smoel2  6547  nnaword  6757  3ecoptocl  6871  rex2dom  7076  sbthlemi10  7249  distrnq0  7790  addassnq0  7793  prcdnql  7815  prcunqu  7816  genpdisj  7854  cauappcvgprlemrnd  7981  caucvgprlemrnd  8004  caucvgprprlemrnd  8032  nn0n0n1ge2b  9675  fzind  9711  icoshft  10342  fzen  10397  seq3coll  11239  shftuz  11527  mulgcd  12737  algcvga  12773  lcmneg  12796  isnmgm  13623  gsummgmpropd  13657  issgrpd  13675  iscmnd  14051  unitmulclb  14359  rmodislmodlem  14624  rmodislmod  14625  blssps  15418  blss  15419  metcnp3  15502  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  iswlkg  16450