Theorem 3expib 1156

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 1152	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp3a 421	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  3anidm12  1241  mob  3076  eqbrrdva  5001  fco  5559  f1oiso2  6031  frxp  6415  onfununi  6562  smoel2  6584  smoiso2  6590  3ecoptocl  6955  dffi2  7386  elfiun  7393  dif1card  7848  infxpenlem  7851  cfeq0  8092  cfsuc  8093  cfflb  8095  cfslb2n  8104  cofsmo  8105  domtriomlem  8278  axdc3lem4  8289  axdc4lem  8291  ttukey2g  8352  tskxpss  8603  grudomon  8648  elnpi  8821  nn0n0n1ge2b  10237  fzind  10324  suprzcl2  10522  icoshft  10975  fzen  11028  hashbclem  11656  seqcoll  11667  shftuz  11839  mulgcd  13001  algcvga  13025  ressbas  13474  resslem  13477  ressress  13481  psss  14601  tsrlemax  14607  spwmo  14613  iscmnd  15379  unitmulclb  15725  isdrngd  15815  issrngd  15904  abvn0b  16317  isphld  16840  fitop  16928  hausnei2  17371  ordtt1  17397  basqtop  17696  filfi  17844  fgcl  17863  neifil  17865  filuni  17870  cnextcn  18051  prdsmet  18353  blssps  18407  blss  18408  metcnp3  18523  hlhil  19297  volsup2  19450  mpfaddcl  19916  mpfmulcl  19917  pf1addcl  19926  pf1mulcl  19927  sincosq1sgn  20359  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  sinq12ge0  20369  bcmono  21014  grpodivf  21787  ipf  22165  sspival  22190  shintcli  22784  spanuni  22999  adjadj  23392  unopadj2  23394  hmopadj  23395  hmopbdoptHIL  23444  esumcocn  24423  ghomf1olem  25058  climuzcnv  25061  dedekind  25140  fness  26252  locfincmp  26274  neificl  26349  metf1o  26351  isismty  26400  ismtybndlem  26405  ablo4pnp  26445  divrngcl  26463  keridl  26532  prnc  26567  ismrcd1  26642  ismrcd2  26643  mzpincl  26681  mzpadd  26685  mzpmul  26686  pellfundge  26835  imasgim  27132  stoweidlem2  27618  stoweidlem17  27633  usg2wlkonot  28080  3cyclfrgrarn1  28116  bnj1379  28908  bnj571  28983  bnj594  28989  bnj580  28990  bnj600  28996  bnj1189  29084  bnj1321  29102  bnj1384  29107  lsmsatcv  29493  llncvrlpln2  30039  lplncvrlvol2  30097  linepsubN  30234  pmapsub  30250  dalawlem10  30362  dalawlem13  30365  dalawlem14  30366  dalaw  30368  diaf11N  31532  dibf11N  31644

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938