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  2985  eqbrrdva  4892  funimaexglem  5404  fco  5491  f1oiso2  5957  caovimo  6205  smoel2  6455  nnaword  6665  3ecoptocl  6779  rex2dom  6979  sbthlemi10  7144  distrnq0  7657  addassnq0  7660  prcdnql  7682  prcunqu  7683  genpdisj  7721  cauappcvgprlemrnd  7848  caucvgprlemrnd  7871  caucvgprprlemrnd  7899  nn0n0n1ge2b  9537  fzind  9573  icoshft  10198  fzen  10251  seq3coll  11077  shftuz  11343  mulgcd  12552  algcvga  12588  lcmneg  12611  isnmgm  13408  gsummgmpropd  13442  issgrpd  13460  iscmnd  13850  unitmulclb  14093  rmodislmodlem  14329  rmodislmod  14330  blssps  15116  blss  15117  metcnp3  15200  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  iswlkg  16070