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  9725  fzind  9761  icoshft  10392  fzen  10447  seq3coll  11294  shftuz  11582  mulgcd  12793  algcvga  12829  lcmneg  12852  isnmgm  13680  issgrpd  13727  iscmnd  14101  unitmulclb  14421  rmodislmodlem  14687  rmodislmod  14688  blssps  15528  blss  15529  metcnp3  15612  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  iswlkg  16570  lealltlt1  16751