Theorem 3expib 1185

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

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

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 962

This theorem is referenced by:  3anidm12  1270  mob  3138  eqbrrdva  5005  fco  5565  f1oiso2  6040  frxp  6681  onfununi  6798  smoel2  6820  smoiso2  6826  3ecoptocl  7188  dffi2  7669  elfiun  7676  dif1card  8173  infxpenlem  8176  cfeq0  8421  cfsuc  8422  cfflb  8424  cfslb2n  8433  cofsmo  8434  domtriomlem  8607  axdc3lem4  8618  axdc4lem  8620  ttukey2g  8681  tskxpss  8935  grudomon  8980  elnpi  9153  dedekind  9529  nn0n0n1ge2b  10640  fzind  10736  suprzcl2  10941  icoshft  11403  fzen  11463  hashbclem  12201  seqcoll  12212  shftuz  12554  mulgcd  13726  algcvga  13750  ressbas  14224  resslem  14227  ressress  14231  psss  15380  tsrlemax  15386  iscmnd  16282  unitmulclb  16747  isdrngd  16837  issrngd  16926  abvn0b  17352  isphld  17983  fitop  18413  hausnei2  18857  ordtt1  18883  basqtop  19184  filfi  19332  fgcl  19351  neifil  19353  filuni  19358  cnextcn  19539  prdsmet  19845  blssps  19899  blss  19900  metcnp3  20015  hlhil  20830  volsup2  20985  mpfaddcl  21452  mpfmulcl  21453  pf1addcl  21462  pf1mulcl  21463  sincosq1sgn  21903  sincosq2sgn  21904  sincosq3sgn  21905  sincosq4sgn  21906  sinq12ge0  21913  bcmono  22559  grpodivf  23652  ipf  24030  sspival  24055  shintcli  24651  spanuni  24866  adjadj  25259  unopadj2  25261  hmopadj  25262  hmopbdoptHIL  25311  resvsca  26218  resvlem  26219  esumcocn  26449  ghomf1olem  27226  climuzcnv  27229  fness  28463  locfincmp  28485  neificl  28558  metf1o  28560  isismty  28609  ismtybndlem  28614  ablo4pnp  28654  divrngcl  28672  keridl  28741  prnc  28776  ismrcd1  28943  ismrcd2  28944  mzpincl  28979  mzpadd  28983  mzpmul  28984  pellfundge  29132  imasgim  29364  stoweidlem2  29706  stoweidlem17  29721  usg2wlkonot  30311  3cyclfrgrarn1  30513  rng1ne0  30673  bnj1379  31641  bnj571  31716  bnj594  31722  bnj580  31723  bnj600  31729  bnj1189  31817  bnj1321  31835  bnj1384  31840  lsmsatcv  32343  llncvrlpln2  32889  lplncvrlvol2  32947  linepsubN  33084  pmapsub  33100  dalawlem10  33212  dalawlem13  33215  dalawlem14  33216  dalaw  33218  diaf11N  34382  dibf11N  34494