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  2999  eqbrrdva  4925  funimaexglem  5439  fco  5527  f1oiso2  6000  caovimo  6248  smoel2  6534  nnaword  6744  3ecoptocl  6858  rex2dom  7063  sbthlemi10  7236  distrnq0  7774  addassnq0  7777  prcdnql  7799  prcunqu  7800  genpdisj  7838  cauappcvgprlemrnd  7965  caucvgprlemrnd  7988  caucvgprprlemrnd  8016  nn0n0n1ge2b  9657  fzind  9693  icoshft  10323  fzen  10377  seq3coll  11214  shftuz  11502  mulgcd  12712  algcvga  12748  lcmneg  12771  isnmgm  13573  gsummgmpropd  13607  issgrpd  13625  iscmnd  14015  unitmulclb  14259  rmodislmodlem  14498  rmodislmod  14499  blssps  15292  blss  15293  metcnp3  15376  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  iswlkg  16324