MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expib Unicode version

Theorem 3expib 1154
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
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1150 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 420 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3anidm12  1239  mob  2960  fco  5414  f1oiso2  5865  frxp  6241  onfununi  6374  smoel2  6396  smoiso2  6402  3ecoptocl  6766  dffi2  7192  elfiun  7199  dif1card  7654  infxpenlem  7657  cfeq0  7898  cfsuc  7899  cfflb  7901  cfslb2n  7910  cofsmo  7911  domtriomlem  8084  axdc3lem4  8095  axdc4lem  8097  ttukey2g  8159  tskxpss  8410  grudomon  8455  elnpi  8628  fzind  10126  suprzcl2  10324  icoshft  10774  fzen  10827  hashbclem  11406  seqcoll  11417  shftuz  11580  mulgcd  12741  algcvga  12765  ressbas  13214  resslem  13217  ressress  13221  psss  14339  tsrlemax  14345  spwmo  14351  iscmnd  15117  unitmulclb  15463  isdrngd  15553  issrngd  15642  abvn0b  16059  isphld  16574  fitop  16662  hausnei2  17097  ordtt1  17123  basqtop  17418  filfi  17570  fgcl  17589  neifil  17591  filuni  17596  prdsmet  17950  blss  17988  metcnp3  18102  hlhil  18823  volsup2  18976  mpfaddcl  19442  mpfmulcl  19443  pf1addcl  19452  pf1mulcl  19453  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  sinq12ge0  19892  bcmono  20532  grpodivf  20929  ipf  21305  sspival  21330  shintcli  21924  spanuni  22139  adjadj  22532  unopadj2  22534  hmopadj  22535  hmopbdoptHIL  22584  esumcocn  23463  ghomf1olem  24016  climuzcnv  24019  dedekind  24097  surjsec2  25223  cur1vald  25302  addvecom  25569  invaddvec  25570  svli2  25587  truni2  25609  inttop2  25618  qusp  25645  intrn  25702  lvsovso  25729  tcnvec  25793  dualded  25886  dualcat2  25887  mrdmcd  25897  cmpassoh  25904  imonclem  25916  ismonc  25917  cmpmon  25918  icmpmon  25919  iepiclem  25926  isepic  25927  idfisf  25944  fness  26385  locfincmp  26407  neificl  26570  metf1o  26572  isismty  26628  ismtybndlem  26633  ablo4pnp  26673  divrngcl  26691  keridl  26760  prnc  26795  ismrcd1  26876  ismrcd2  26877  mzpincl  26915  mzpadd  26919  mzpmul  26920  pellfundge  27070  imasgim  27367  stoweidlem2  27854  stoweidlem17  27869  3cyclfrgrarn1  28435  bnj1379  29179  bnj571  29254  bnj594  29260  bnj580  29261  bnj600  29267  bnj1189  29355  bnj1321  29373  bnj1384  29378  lsmsatcv  29822  llncvrlpln2  30368  lplncvrlvol2  30426  linepsubN  30563  pmapsub  30579  dalawlem10  30691  dalawlem13  30694  dalawlem14  30695  dalaw  30697  diaf11N  31861  dibf11N  31973
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator