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  2942  eqbrrdva  4832  funimaexglem  5337  fco  5419  f1oiso2  5870  caovimo  6112  smoel2  6356  nnaword  6564  3ecoptocl  6678  sbthlemi10  7025  distrnq0  7519  addassnq0  7522  prcdnql  7544  prcunqu  7545  genpdisj  7583  cauappcvgprlemrnd  7710  caucvgprlemrnd  7733  caucvgprprlemrnd  7761  nn0n0n1ge2b  9396  fzind  9432  icoshft  10056  fzen  10109  seq3coll  10913  shftuz  10961  mulgcd  12153  algcvga  12189  lcmneg  12212  isnmgm  12943  gsummgmpropd  12977  issgrpd  12995  iscmnd  13368  unitmulclb  13610  rmodislmodlem  13846  rmodislmod  13847  blssps  14595  blss  14596  metcnp3  14679  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964