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  7827  addassnq0  7830  prcdnql  7852  prcunqu  7853  genpdisj  7891  cauappcvgprlemrnd  8018  caucvgprlemrnd  8041  caucvgprprlemrnd  8069  nn0n0n1ge2b  9730  fzind  9766  icoshft  10403  fzen  10458  seq3coll  11310  shftuz  11598  mulgcd  12812  algcvga  12848  lcmneg  12871  isnmgm  13733  issgrpd  13780  iscmnd  14185  unitmulclb  14505  rmodislmodlem  14771  rmodislmod  14772  blssps  15619  blss  15620  metcnp3  15703  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  bcmono  16265  iswlkg  16736  lealltlt1  16917