Theorem 3expib 1232

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

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

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 1006

This theorem is referenced by:  3anidm12  1331  mob  2987  eqbrrdva  4899  funimaexglem  5412  fco  5499  f1oiso2  5970  caovimo  6218  smoel2  6471  nnaword  6681  3ecoptocl  6795  rex2dom  6998  sbthlemi10  7167  distrnq0  7681  addassnq0  7684  prcdnql  7706  prcunqu  7707  genpdisj  7745  cauappcvgprlemrnd  7872  caucvgprlemrnd  7895  caucvgprprlemrnd  7923  nn0n0n1ge2b  9561  fzind  9597  icoshft  10227  fzen  10280  seq3coll  11109  shftuz  11397  mulgcd  12607  algcvga  12643  lcmneg  12666  isnmgm  13463  gsummgmpropd  13497  issgrpd  13515  iscmnd  13905  unitmulclb  14149  rmodislmodlem  14385  rmodislmod  14386  blssps  15177  blss  15178  metcnp3  15261  sincosq1sgn  15576  sincosq2sgn  15577  sincosq3sgn  15578  sincosq4sgn  15579  iswlkg  16206