Theorem 3expib 1232

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

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 1006

This theorem is referenced by:  3anidm12  1331  mob  2988  eqbrrdva  4900  funimaexglem  5413  fco  5500  f1oiso2  5967  caovimo  6215  smoel2  6468  nnaword  6678  3ecoptocl  6792  rex2dom  6995  sbthlemi10  7164  distrnq0  7678  addassnq0  7681  prcdnql  7703  prcunqu  7704  genpdisj  7742  cauappcvgprlemrnd  7869  caucvgprlemrnd  7892  caucvgprprlemrnd  7920  nn0n0n1ge2b  9558  fzind  9594  icoshft  10224  fzen  10277  seq3coll  11105  shftuz  11377  mulgcd  12586  algcvga  12622  lcmneg  12645  isnmgm  13442  gsummgmpropd  13476  issgrpd  13494  iscmnd  13884  unitmulclb  14127  rmodislmodlem  14363  rmodislmod  14364  blssps  15150  blss  15151  metcnp3  15234  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  iswlkg  16179