Theorem 3expib 1206

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

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

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 980

This theorem is referenced by:  3anidm12  1295  mob  2920  eqbrrdva  4798  funimaexglem  5300  fco  5382  f1oiso2  5828  caovimo  6068  smoel2  6304  nnaword  6512  3ecoptocl  6624  sbthlemi10  6965  distrnq0  7458  addassnq0  7461  prcdnql  7483  prcunqu  7484  genpdisj  7522  cauappcvgprlemrnd  7649  caucvgprlemrnd  7672  caucvgprprlemrnd  7700  nn0n0n1ge2b  9332  fzind  9368  icoshft  9990  fzen  10043  seq3coll  10822  shftuz  10826  mulgcd  12017  algcvga  12051  lcmneg  12074  isnmgm  12779  iscmnd  13101  unitmulclb  13283  rmodislmodlem  13440  rmodislmod  13441  blssps  13930  blss  13931  metcnp3  14014  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253