Theorem 3expib 1206

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

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

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 980

This theorem is referenced by:  3anidm12  1295  mob  2919  eqbrrdva  4797  funimaexglem  5299  fco  5381  f1oiso2  5827  caovimo  6067  smoel2  6303  nnaword  6511  3ecoptocl  6623  sbthlemi10  6964  distrnq0  7457  addassnq0  7460  prcdnql  7482  prcunqu  7483  genpdisj  7521  cauappcvgprlemrnd  7648  caucvgprlemrnd  7671  caucvgprprlemrnd  7699  nn0n0n1ge2b  9330  fzind  9366  icoshft  9988  fzen  10040  seq3coll  10817  shftuz  10821  mulgcd  12011  algcvga  12045  lcmneg  12068  isnmgm  12733  iscmnd  13054  unitmulclb  13236  blssps  13820  blss  13821  metcnp3  13904  sincosq1sgn  14140  sincosq2sgn  14141  sincosq3sgn  14142  sincosq4sgn  14143