Theorem 3expib 1208

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

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

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 982

This theorem is referenced by:  3anidm12  1306  mob  2946  eqbrrdva  4837  funimaexglem  5342  fco  5426  f1oiso2  5877  caovimo  6121  smoel2  6370  nnaword  6578  3ecoptocl  6692  sbthlemi10  7041  distrnq0  7543  addassnq0  7546  prcdnql  7568  prcunqu  7569  genpdisj  7607  cauappcvgprlemrnd  7734  caucvgprlemrnd  7757  caucvgprprlemrnd  7785  nn0n0n1ge2b  9422  fzind  9458  icoshft  10082  fzen  10135  seq3coll  10951  shftuz  10999  mulgcd  12208  algcvga  12244  lcmneg  12267  isnmgm  13062  gsummgmpropd  13096  issgrpd  13114  iscmnd  13504  unitmulclb  13746  rmodislmodlem  13982  rmodislmod  13983  blssps  14747  blss  14748  metcnp3  14831  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149