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  2943  eqbrrdva  4833  funimaexglem  5338  fco  5420  f1oiso2  5871  caovimo  6114  smoel2  6358  nnaword  6566  3ecoptocl  6680  sbthlemi10  7027  distrnq0  7521  addassnq0  7524  prcdnql  7546  prcunqu  7547  genpdisj  7585  cauappcvgprlemrnd  7712  caucvgprlemrnd  7735  caucvgprprlemrnd  7763  nn0n0n1ge2b  9399  fzind  9435  icoshft  10059  fzen  10112  seq3coll  10916  shftuz  10964  mulgcd  12156  algcvga  12192  lcmneg  12215  isnmgm  12946  gsummgmpropd  12980  issgrpd  12998  iscmnd  13371  unitmulclb  13613  rmodislmodlem  13849  rmodislmod  13850  blssps  14606  blss  14607  metcnp3  14690  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005