Theorem 3expib 1199

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

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

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

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

This theorem is referenced by:  3anidm12  1285  mob  3285  eqbrrdva  5172  fco  5741  f1oiso2  6236  frxp  6893  onfununi  7012  smoel2  7034  smoiso2  7040  3ecoptocl  7403  dffi2  7883  elfiun  7890  dif1card  8388  infxpenlem  8391  cfeq0  8636  cfsuc  8637  cfflb  8639  cfslb2n  8648  cofsmo  8649  domtriomlem  8822  axdc3lem4  8833  axdc4lem  8835  ttukey2g  8896  tskxpss  9150  grudomon  9195  elnpi  9366  dedekind  9743  nn0n0n1ge2b  10860  fzind  10959  suprzcl2  11172  icoshft  11642  fzen  11703  hashbclem  12467  seqcoll  12478  shftuz  12865  mulgcd  14043  algcvga  14067  ressbas  14545  resslem  14548  ressress  14552  psss  15701  tsrlemax  15707  iscmnd  16616  rng1ne0  17040  unitmulclb  17115  isdrngd  17221  issrngd  17310  abvn0b  17750  mpfaddcl  18002  mpfmulcl  18003  pf1addcl  18188  pf1mulcl  18189  isphld  18484  fitop  19204  hausnei2  19648  ordtt1  19674  basqtop  19975  filfi  20123  fgcl  20142  neifil  20144  filuni  20149  cnextcn  20330  prdsmet  20636  blssps  20690  blss  20691  metcnp3  20806  hlhil  21621  volsup2  21777  sincosq1sgn  22652  sincosq2sgn  22653  sincosq3sgn  22654  sincosq4sgn  22655  sinq12ge0  22662  bcmono  23308  usg2wlkonot  24587  3cyclfrgrarn1  24716  grpodivf  24952  ipf  25330  sspival  25355  shintcli  25951  spanuni  26166  adjadj  26559  unopadj2  26561  hmopadj  26562  hmopbdoptHIL  26611  resvsca  27511  resvlem  27512  esumcocn  27754  ghomf1olem  28537  climuzcnv  28540  fness  29782  locfincmp  29804  neificl  29877  metf1o  29879  isismty  29928  ismtybndlem  29933  ablo4pnp  29973  divrngcl  29991  keridl  30060  prnc  30095  ismrcd1  30262  ismrcd2  30263  mzpincl  30298  mzpadd  30302  mzpmul  30303  pellfundge  30450  imasgim  30680  lcmneg  30837  stoweidlem2  31330  stoweidlem17  31345  uhgrauhgbi  31869  bnj1379  32986  bnj571  33061  bnj594  33067  bnj580  33068  bnj600  33074  bnj1189  33162  bnj1321  33180  bnj1384  33185  lsmsatcv  33825  llncvrlpln2  34371  lplncvrlvol2  34429  linepsubN  34566  pmapsub  34582  dalawlem10  34694  dalawlem13  34697  dalawlem14  34698  dalaw  34700  diaf11N  35864  dibf11N  35976