Theorem 3expib 1237

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anidm12  1336  mob  3008  eqbrrdva  4952  funimaexglem  5467  fco  5555  f1oiso2  6036  caovimo  6286  smoel2  6578  nnaword  6788  3ecoptocl  6902  rex2dom  7114  sbthlemi10  7288  distrnq0  7832  addassnq0  7835  prcdnql  7857  prcunqu  7858  genpdisj  7896  cauappcvgprlemrnd  8023  caucvgprlemrnd  8046  caucvgprprlemrnd  8074  nn0n0n1ge2b  9736  fzind  9772  icoshft  10409  fzen  10464  seq3coll  11316  shftuz  11604  mulgcd  12818  algcvga  12854  lcmneg  12877  isnmgm  13739  issgrpd  13786  iscmnd  14191  unitmulclb  14530  rmodislmodlem  14796  rmodislmod  14797  blssps  15653  blss  15654  metcnp3  15737  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  bcmono  16304  iswlkg  16775  lealltlt1  16956