Theorem 3expib 1201

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3anidm12  1290  mob  2912  eqbrrdva  4781  funimaexglem  5281  fco  5363  f1oiso2  5806  caovimo  6046  smoel2  6282  nnaword  6490  3ecoptocl  6602  sbthlemi10  6943  distrnq0  7421  addassnq0  7424  prcdnql  7446  prcunqu  7447  genpdisj  7485  cauappcvgprlemrnd  7612  caucvgprlemrnd  7635  caucvgprprlemrnd  7663  nn0n0n1ge2b  9291  fzind  9327  icoshft  9947  fzen  9999  seq3coll  10777  shftuz  10781  mulgcd  11971  algcvga  12005  lcmneg  12028  isnmgm  12614  blssps  13221  blss  13222  metcnp3  13305  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544