Theorem 3expib 1188

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

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

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 965

This theorem is referenced by:  3anidm12  1277  mob  2894  eqbrrdva  4753  funimaexglem  5250  fco  5332  f1oiso2  5772  caovimo  6008  smoel2  6244  nnaword  6451  3ecoptocl  6562  sbthlemi10  6903  distrnq0  7362  addassnq0  7365  prcdnql  7387  prcunqu  7388  genpdisj  7426  cauappcvgprlemrnd  7553  caucvgprlemrnd  7576  caucvgprprlemrnd  7604  nn0n0n1ge2b  9226  fzind  9262  icoshft  9876  fzen  9927  seq3coll  10695  shftuz  10699  mulgcd  11880  algcvga  11908  lcmneg  11931  blssps  12787  blss  12788  metcnp3  12871  sincosq1sgn  13107  sincosq2sgn  13108  sincosq3sgn  13109  sincosq4sgn  13110