Theorem 3expib 1209

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

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

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 983

This theorem is referenced by:  3anidm12  1308  mob  2962  eqbrrdva  4866  funimaexglem  5376  fco  5461  f1oiso2  5919  caovimo  6163  smoel2  6412  nnaword  6620  3ecoptocl  6734  rex2dom  6934  sbthlemi10  7094  distrnq0  7607  addassnq0  7610  prcdnql  7632  prcunqu  7633  genpdisj  7671  cauappcvgprlemrnd  7798  caucvgprlemrnd  7821  caucvgprprlemrnd  7849  nn0n0n1ge2b  9487  fzind  9523  icoshft  10147  fzen  10200  seq3coll  11024  shftuz  11243  mulgcd  12452  algcvga  12488  lcmneg  12511  isnmgm  13307  gsummgmpropd  13341  issgrpd  13359  iscmnd  13749  unitmulclb  13991  rmodislmodlem  14227  rmodislmod  14228  blssps  15014  blss  15015  metcnp3  15098  sincosq1sgn  15413  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416