Theorem 3expib 1237

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anidm12  1336  mob  3008  eqbrrdva  4950  funimaexglem  5464  fco  5552  f1oiso2  6033  caovimo  6283  smoel2  6574  nnaword  6784  3ecoptocl  6898  rex2dom  7110  sbthlemi10  7283  distrnq0  7826  addassnq0  7829  prcdnql  7851  prcunqu  7852  genpdisj  7890  cauappcvgprlemrnd  8017  caucvgprlemrnd  8040  caucvgprprlemrnd  8068  nn0n0n1ge2b  9729  fzind  9765  icoshft  10402  fzen  10457  seq3coll  11308  shftuz  11596  mulgcd  12809  algcvga  12845  lcmneg  12868  isnmgm  13729  issgrpd  13776  iscmnd  14150  unitmulclb  14470  rmodislmodlem  14736  rmodislmod  14737  blssps  15577  blss  15578  metcnp3  15661  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  bcmono  16202  iswlkg  16668  lealltlt1  16849