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  4952  funimaexglem  5467  fco  5555  f1oiso2  6036  caovimo  6286  smoel2  6579  nnaword  6789  3ecoptocl  6903  rex2dom  7116  sbthlemi10  7290  distrnq0  7832  addassnq0  7835  prcdnql  7857  prcunqu  7858  genpdisj  7896  cauappcvgprlemrnd  8023  caucvgprlemrnd  8046  caucvgprprlemrnd  8074  nn0n0n1ge2b  9734  fzind  9771  icoshft  10408  fzen  10463  seq3coll  11315  shftuz  11603  mulgcd  12817  algcvga  12853  lcmneg  12876  isnmgm  13738  issgrpd  13785  iscmnd  14190  unitmulclb  14529  rmodislmodlem  14795  rmodislmod  14796  blssps  15670  blss  15671  metcnp3  15754  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  bcmono  16321  iswlkg  16792  lealltlt1  16973