Theorem 3expib 1141

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3anidm12  1226  mob  2774  eqbrrdva  4523  funimaexglem  5002  fco  5076  f1oiso2  5486  caovimo  5714  smoel2  5941  nnaword  6107  3ecoptocl  6218  distrnq0  6649  addassnq0  6652  prcdnql  6674  prcunqu  6675  genpdisj  6713  cauappcvgprlemrnd  6840  caucvgprlemrnd  6863  caucvgprprlemrnd  6891  nn0n0n1ge2b  8427  fzind  8462  icoshft  9012  fzen  9062  shftuz  9705  mulgcd  10405  ialgcvga  10433  lcmneg  10456