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  1307  mob  2954  eqbrrdva  4847  funimaexglem  5356  fco  5440  f1oiso2  5895  caovimo  6139  smoel2  6388  nnaword  6596  3ecoptocl  6710  rex2dom  6909  sbthlemi10  7067  distrnq0  7571  addassnq0  7574  prcdnql  7596  prcunqu  7597  genpdisj  7635  cauappcvgprlemrnd  7762  caucvgprlemrnd  7785  caucvgprprlemrnd  7813  nn0n0n1ge2b  9451  fzind  9487  icoshft  10111  fzen  10164  seq3coll  10985  shftuz  11099  mulgcd  12308  algcvga  12344  lcmneg  12367  isnmgm  13163  gsummgmpropd  13197  issgrpd  13215  iscmnd  13605  unitmulclb  13847  rmodislmodlem  14083  rmodislmod  14084  blssps  14870  blss  14871  metcnp3  14954  sincosq1sgn  15269  sincosq2sgn  15270  sincosq3sgn  15271  sincosq4sgn  15272