Theorem 3expib 1196

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  3anidm12  1285  mob  2908  eqbrrdva  4774  funimaexglem  5271  fco  5353  f1oiso2  5795  caovimo  6035  smoel2  6271  nnaword  6479  3ecoptocl  6590  sbthlemi10  6931  distrnq0  7400  addassnq0  7403  prcdnql  7425  prcunqu  7426  genpdisj  7464  cauappcvgprlemrnd  7591  caucvgprlemrnd  7614  caucvgprprlemrnd  7642  nn0n0n1ge2b  9270  fzind  9306  icoshft  9926  fzen  9978  seq3coll  10755  shftuz  10759  mulgcd  11949  algcvga  11983  lcmneg  12006  isnmgm  12591  blssps  13067  blss  13068  metcnp3  13151  sincosq1sgn  13387  sincosq2sgn  13388  sincosq3sgn  13389  sincosq4sgn  13390