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  2955  eqbrrdva  4848  funimaexglem  5357  fco  5441  f1oiso2  5896  caovimo  6140  smoel2  6389  nnaword  6597  3ecoptocl  6711  rex2dom  6910  sbthlemi10  7068  distrnq0  7572  addassnq0  7575  prcdnql  7597  prcunqu  7598  genpdisj  7636  cauappcvgprlemrnd  7763  caucvgprlemrnd  7786  caucvgprprlemrnd  7814  nn0n0n1ge2b  9452  fzind  9488  icoshft  10112  fzen  10165  seq3coll  10987  shftuz  11128  mulgcd  12337  algcvga  12373  lcmneg  12396  isnmgm  13192  gsummgmpropd  13226  issgrpd  13244  iscmnd  13634  unitmulclb  13876  rmodislmodlem  14112  rmodislmod  14113  blssps  14899  blss  14900  metcnp3  14983  sincosq1sgn  15298  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301