Theorem 3expib 1230

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

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

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 1004

This theorem is referenced by:  3anidm12  1329  mob  2986  eqbrrdva  4898  funimaexglem  5410  fco  5497  f1oiso2  5963  caovimo  6211  smoel2  6464  nnaword  6674  3ecoptocl  6788  rex2dom  6991  sbthlemi10  7156  distrnq0  7669  addassnq0  7672  prcdnql  7694  prcunqu  7695  genpdisj  7733  cauappcvgprlemrnd  7860  caucvgprlemrnd  7883  caucvgprprlemrnd  7911  nn0n0n1ge2b  9549  fzind  9585  icoshft  10215  fzen  10268  seq3coll  11096  shftuz  11368  mulgcd  12577  algcvga  12613  lcmneg  12636  isnmgm  13433  gsummgmpropd  13467  issgrpd  13485  iscmnd  13875  unitmulclb  14118  rmodislmodlem  14354  rmodislmod  14355  blssps  15141  blss  15142  metcnp3  15225  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  iswlkg  16126