Theorem 3expib 1233

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

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

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 1007

This theorem is referenced by:  3anidm12  1332  mob  2989  eqbrrdva  4906  funimaexglem  5420  fco  5507  f1oiso2  5978  caovimo  6226  smoel2  6512  nnaword  6722  3ecoptocl  6836  rex2dom  7039  sbthlemi10  7208  distrnq0  7722  addassnq0  7725  prcdnql  7747  prcunqu  7748  genpdisj  7786  cauappcvgprlemrnd  7913  caucvgprlemrnd  7936  caucvgprprlemrnd  7964  nn0n0n1ge2b  9603  fzind  9639  icoshft  10269  fzen  10323  seq3coll  11152  shftuz  11440  mulgcd  12650  algcvga  12686  lcmneg  12709  isnmgm  13506  gsummgmpropd  13540  issgrpd  13558  iscmnd  13948  unitmulclb  14192  rmodislmodlem  14429  rmodislmod  14430  blssps  15221  blss  15222  metcnp3  15305  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  iswlkg  16253