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  2947  fco  5398  f1oiso2  5849  frxp  6225  onfununi  6358  smoel2  6380  smoiso2  6386  3ecoptocl  6750  dffi2  7176  elfiun  7183  dif1card  7638  infxpenlem  7641  cfeq0  7882  cfsuc  7883  cfflb  7885  cfslb2n  7894  cofsmo  7895  domtriomlem  8068  axdc3lem4  8079  axdc4lem  8081  ttukey2g  8143  tskxpss  8394  grudomon  8439  elnpi  8612  fzind  10110  suprzcl2  10308  icoshft  10758  fzen  10811  hashbclem  11390  seqcoll  11401  shftuz  11564  mulgcd  12725  algcvga  12749  ressbas  13198  resslem  13201  ressress  13205  psss  14323  tsrlemax  14329  spwmo  14335  iscmnd  15101  unitmulclb  15447  isdrngd  15537  issrngd  15626  abvn0b  16043  isphld  16558  fitop  16646  hausnei2  17081  ordtt1  17107  basqtop  17402  filfi  17554  fgcl  17573  neifil  17575  filuni  17580  prdsmet  17934  blss  17972  metcnp3  18086  hlhil  18807  volsup2  18960  mpfaddcl  19426  mpfmulcl  19427  pf1addcl  19436  pf1mulcl  19437  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  sinq12ge0  19876  bcmono  20516  grpodivf  20913  ipf  21289  sspival  21314  shintcli  21908  spanuni  22123  adjadj  22516  unopadj2  22518  hmopadj  22519  hmopbdoptHIL  22568  esumcocn  23448  ghomf1olem  24001  climuzcnv  24004  dedekind  24082  surjsec2  25120  cur1vald  25199  addvecom  25466  invaddvec  25467  svli2  25484  truni2  25506  inttop2  25515  qusp  25542  intrn  25599  lvsovso  25626  tcnvec  25690  dualded  25783  dualcat2  25784  mrdmcd  25794  cmpassoh  25801  imonclem  25813  ismonc  25814  cmpmon  25815  icmpmon  25816  iepiclem  25823  isepic  25824  idfisf  25841  fness  26282  locfincmp  26304  neificl  26467  metf1o  26469  isismty  26525  ismtybndlem  26530  ablo4pnp  26570  divrngcl  26588  keridl  26657  prnc  26692  ismrcd1  26773  ismrcd2  26774  mzpincl  26812  mzpadd  26816  mzpmul  26817  pellfundge  26967  imasgim  27264  stoweidlem2  27751  stoweidlem17  27766  bnj1379  28863  bnj571  28938  bnj594  28944  bnj580  28945  bnj600  28951  bnj1189  29039  bnj1321  29057  bnj1384  29062  lsmsatcv  29200  llncvrlpln2  29746  lplncvrlvol2  29804  linepsubN  29941  pmapsub  29957  dalawlem10  30069  dalawlem13  30072  dalawlem14  30073  dalaw  30075  diaf11N  31239  dibf11N  31351
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