Theorem 3expib 1184

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

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

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 964

This theorem is referenced by:  3anidm12  1273  mob  2866  eqbrrdva  4709  funimaexglem  5206  fco  5288  f1oiso2  5728  caovimo  5964  smoel2  6200  nnaword  6407  3ecoptocl  6518  sbthlemi10  6854  distrnq0  7267  addassnq0  7270  prcdnql  7292  prcunqu  7293  genpdisj  7331  cauappcvgprlemrnd  7458  caucvgprlemrnd  7481  caucvgprprlemrnd  7509  nn0n0n1ge2b  9130  fzind  9166  icoshft  9773  fzen  9823  seq3coll  10585  shftuz  10589  mulgcd  11704  algcvga  11732  lcmneg  11755  blssps  12596  blss  12597  metcnp3  12680  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910