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

Theorem 3expib 1157
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 1153 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp3a 422 1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3anidm12  1242  mob  3118  eqbrrdva  5044  fco  5602  f1oiso2  6074  frxp  6458  onfununi  6605  smoel2  6627  smoiso2  6633  3ecoptocl  6998  dffi2  7430  elfiun  7437  dif1card  7894  infxpenlem  7897  cfeq0  8138  cfsuc  8139  cfflb  8141  cfslb2n  8150  cofsmo  8151  domtriomlem  8324  axdc3lem4  8335  axdc4lem  8337  ttukey2g  8398  tskxpss  8649  grudomon  8694  elnpi  8867  nn0n0n1ge2b  10283  fzind  10370  suprzcl2  10568  icoshft  11021  fzen  11074  hashbclem  11703  seqcoll  11714  shftuz  11886  mulgcd  13048  algcvga  13072  ressbas  13521  resslem  13524  ressress  13528  psss  14648  tsrlemax  14654  spwmo  14660  iscmnd  15426  unitmulclb  15772  isdrngd  15862  issrngd  15951  abvn0b  16364  isphld  16887  fitop  16975  hausnei2  17419  ordtt1  17445  basqtop  17745  filfi  17893  fgcl  17912  neifil  17914  filuni  17919  cnextcn  18100  prdsmet  18402  blssps  18456  blss  18457  metcnp3  18572  hlhil  19346  volsup2  19499  mpfaddcl  19965  mpfmulcl  19966  pf1addcl  19975  pf1mulcl  19976  sincosq1sgn  20408  sincosq2sgn  20409  sincosq3sgn  20410  sincosq4sgn  20411  sinq12ge0  20418  bcmono  21063  grpodivf  21836  ipf  22214  sspival  22239  shintcli  22833  spanuni  23048  adjadj  23441  unopadj2  23443  hmopadj  23444  hmopbdoptHIL  23493  esumcocn  24472  ghomf1olem  25107  climuzcnv  25110  dedekind  25189  fness  26364  locfincmp  26386  neificl  26461  metf1o  26463  isismty  26512  ismtybndlem  26517  ablo4pnp  26557  divrngcl  26575  keridl  26644  prnc  26679  ismrcd1  26754  ismrcd2  26755  mzpincl  26793  mzpadd  26797  mzpmul  26798  pellfundge  26947  imasgim  27243  stoweidlem2  27729  stoweidlem17  27744  usg2wlkonot  28352  3cyclfrgrarn1  28404  bnj1379  29204  bnj571  29279  bnj594  29285  bnj580  29286  bnj600  29292  bnj1189  29380  bnj1321  29398  bnj1384  29403  lsmsatcv  29810  llncvrlpln2  30356  lplncvrlvol2  30414  linepsubN  30551  pmapsub  30567  dalawlem10  30679  dalawlem13  30682  dalawlem14  30683  dalaw  30685  diaf11N  31849  dibf11N  31961
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator