Theorem 3expib 1190

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

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

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 967

This theorem is referenced by:  3anidm12  1275  mob  3141  eqbrrdva  5009  fco  5568  f1oiso2  6043  frxp  6682  onfununi  6802  smoel2  6824  smoiso2  6830  3ecoptocl  7192  dffi2  7673  elfiun  7680  dif1card  8177  infxpenlem  8180  cfeq0  8425  cfsuc  8426  cfflb  8428  cfslb2n  8437  cofsmo  8438  domtriomlem  8611  axdc3lem4  8622  axdc4lem  8624  ttukey2g  8685  tskxpss  8939  grudomon  8984  elnpi  9157  dedekind  9533  nn0n0n1ge2b  10644  fzind  10740  suprzcl2  10945  icoshft  11407  fzen  11467  hashbclem  12205  seqcoll  12216  shftuz  12558  mulgcd  13730  algcvga  13754  ressbas  14228  resslem  14231  ressress  14235  psss  15384  tsrlemax  15390  iscmnd  16289  unitmulclb  16757  isdrngd  16857  issrngd  16946  abvn0b  17374  mpfaddcl  17620  mpfmulcl  17621  pf1addcl  17787  pf1mulcl  17788  isphld  18083  fitop  18513  hausnei2  18957  ordtt1  18983  basqtop  19284  filfi  19432  fgcl  19451  neifil  19453  filuni  19458  cnextcn  19639  prdsmet  19945  blssps  19999  blss  20000  metcnp3  20115  hlhil  20930  volsup2  21085  sincosq1sgn  21960  sincosq2sgn  21961  sincosq3sgn  21962  sincosq4sgn  21963  sinq12ge0  21970  bcmono  22616  grpodivf  23733  ipf  24111  sspival  24136  shintcli  24732  spanuni  24947  adjadj  25340  unopadj2  25342  hmopadj  25343  hmopbdoptHIL  25392  resvsca  26298  resvlem  26299  esumcocn  26529  ghomf1olem  27313  climuzcnv  27316  fness  28554  locfincmp  28576  neificl  28649  metf1o  28651  isismty  28700  ismtybndlem  28705  ablo4pnp  28745  divrngcl  28763  keridl  28832  prnc  28867  ismrcd1  29034  ismrcd2  29035  mzpincl  29070  mzpadd  29074  mzpmul  29075  pellfundge  29223  imasgim  29455  stoweidlem2  29797  stoweidlem17  29812  usg2wlkonot  30402  3cyclfrgrarn1  30604  rng1ne0  30773  bnj1379  31824  bnj571  31899  bnj594  31905  bnj580  31906  bnj600  31912  bnj1189  32000  bnj1321  32018  bnj1384  32023  lsmsatcv  32655  llncvrlpln2  33201  lplncvrlvol2  33259  linepsubN  33396  pmapsub  33412  dalawlem10  33524  dalawlem13  33527  dalawlem14  33528  dalaw  33530  diaf11N  34694  dibf11N  34806