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 ) )

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

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 1011

This theorem is referenced by:  3anidm12  1336  mob  3008  eqbrrdva  4945  funimaexglem  5459  fco  5547  f1oiso2  6023  caovimo  6273  smoel2  6564  nnaword  6774  3ecoptocl  6888  rex2dom  7100  sbthlemi10  7273  distrnq0  7816  addassnq0  7819  prcdnql  7841  prcunqu  7842  genpdisj  7880  cauappcvgprlemrnd  8007  caucvgprlemrnd  8030  caucvgprprlemrnd  8058  nn0n0n1ge2b  9704  fzind  9740  icoshft  10371  fzen  10426  seq3coll  11272  shftuz  11560  mulgcd  12771  algcvga  12807  lcmneg  12830  isnmgm  13657  issgrpd  13704  iscmnd  14078  unitmulclb  14394  rmodislmodlem  14659  rmodislmod  14660  blssps  15451  blss  15452  metcnp3  15535  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  iswlkg  16484  lealltlt1  16665