Theorem 3expib 1107

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

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3anidm12  1192  mob  2723  eqbrrdva  4505  funimaexglem  4982  fco  5056  f1oiso2  5466  caovimo  5694  smoel2  5918  nnaword  6084  3ecoptocl  6195  distrnq0  6557  addassnq0  6560  prcdnql  6582  prcunqu  6583  genpdisj  6621  cauappcvgprlemrnd  6748  caucvgprlemrnd  6771  caucvgprprlemrnd  6799  nn0n0n1ge2b  8320  fzind  8353  icoshft  8858  fzen  8907  shftuz  9418  ialgcvga  9890