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

Theorem 3impa 1186
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3impa  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 604 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1185 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  3impdir  1279  syl3an9b  1292  biimp3a  1323  thema3  1588  rspec3  2830  rspc3v  3219  raltpg  4071  rextpg  4072  disjiun  4430  opelopabt  4752  ordelinel  4969  3optocl  5069  fun2ssres  5620  funssfv  5872  foco2  6032  f1elima  6150  ot1stg  6788  ot2ndg  6789  smogt  7028  omord2  7206  omword  7209  omass  7219  oeword  7229  nnmass  7263  omabslem  7285  ecovass  7408  fpmg  7434  f1imaeng  7565  findcard  7748  cdaun  8541  cfsmolem  8639  ingru  9182  addasspi  9262  mulasspi  9264  ltapi  9270  ltmpi  9271  genpass  9376  axpre-ltadd  9533  adddir  9576  leltne  9663  le2tri3i  9703  dedekind  9732  addsub12  9822  subdir  9980  ltaddsub  10015  leaddsub  10017  recextlem2  10169  div12  10218  divdiv32  10241  divdiv1  10244  lble  10484  fnn0ind  10949  supminf  11158  xrleltne  11340  xrmaxeq  11369  xrmineq  11370  iccgelb  11570  elicc4  11580  iccsplit  11642  elfz  11667  fzrevral  11751  fldiv2  11944  modabs  11985  modsubdir  12011  expgt0  12154  expge0  12157  expge1  12158  mulexpz  12161  expp1z  12169  expm1  12170  digit2  12254  digit1  12255  faclbnd4  12330  faclbnd5  12331  ccatval1  12547  abssubne0  13098  absdiflt  13099  absdifle  13100  binom  13594  cos01gt0  13776  rpnnen2lem4  13801  dvds0lem  13844  dvdsnegb  13851  muldvds1  13858  muldvds2  13859  dvdscmulr  13862  dvdsmulcr  13863  gcdaddm  14015  prmdvdsexp  14103  rpexp1i  14110  monpropd  14982  prfval  15315  xpcpropd  15324  curf2ndf  15363  lubub  15595  lubl  15596  eqglact  16040  mndodcongi  16356  oddvdsnn0  16357  efgi0  16527  efgi1  16528  lss0cl  17369  ipcl  18428  scmatscmid  18768  pmatcollpw3fi1lem1  19047  opnneiss  19378  cnpval  19496  cnf2  19509  cnnei  19542  llyi  19734  nllyi  19735  ptpjcn  19840  cnmptk2  19915  flfval  20219  cnmpt2plusg  20315  cnmpt2vsca  20425  ustincl  20438  xbln0  20645  blssec  20666  blpnfctr  20667  mopni2  20724  mopni3  20725  nmoval  20950  nmocl  20955  isnghm2  20959  isnmhm2  20987  cnmpt2ds  21076  metdseq0  21086  cnmpt2ip  21416  caucfil  21450  mbfimasn  21769  dvnf  22058  dvnbss  22059  coemul  22376  dvply1  22407  dvnply2  22410  pserdvlem2  22550  logeftb  22689  advlogexp  22757  cxpne0  22779  cxpp1  22782  logrec  22872  lgsne0  23329  f1otrg  23843  ax5seglem9  23909  umgrass  23982  umgran0  23983  umgrale  23984  nbgraf1olem3  24105  pthdepisspth  24238  grposn  24879  issubgoi  24974  ablomul  25019  sspval  25298  sspnval  25312  lnof  25332  lnocoi  25334  nmooval  25340  nmooge0  25344  nmoub3i  25350  bloln  25361  nmblore  25363  hvaddsubass  25620  hvmulcan2  25652  hhssnv  25842  hosval  26321  homval  26322  hodval  26323  hfsval  26324  hfmval  26325  homco1  26382  homulass  26383  hoadddir  26385  hoaddsubass  26396  hosubsub4  26399  nmopub2tALT  26490  nmfnleub2  26507  kbval  26535  lnopmul  26548  lnopmulsubi  26557  0lnfn  26566  lnopcoi  26584  nmcoplb  26611  nmcfnlb  26635  kbass2  26698  nmopleid  26720  hstoh  26813  mdi  26876  dmdi  26883  dmdi4  26888  mdsl3  26897  cdj3lem2  27016  ffs2  27209  supxrnemnf  27237  reofld  27479  elno2  28977  ftc1anclem2  29655  fnessex  29734  fzmul  29823  incsequz2  29832  nninfnub  29834  exidreslem  29929  ghomf  29934  rngohomf  29959  rngohom1  29961  rngohomadd  29962  rngohommul  29963  rngoiso1o  29972  rngoisohom  29973  igenmin  30051  3anrabdioph  30307  3orrabdioph  30308  rencldnfilem  30345  expmordi  30474  divalgmodcl  30522  jm2.18  30523  jm2.25  30534  jm2.15nn0  30538  addrfv  30911  subrfv  30912  mulvfv  30913  ssfiunibd  31041  stoweidlem34  31289  stoweidlem48  31303  aovmpt4g  31708  ccatw2s1cl  31772  bi3impa  32207  bnj563  32754  bnj605  32919  bnj607  32928  bnj1097  32991  lkrcl  33764  lkrf0  33765  omlfh1N  33930  tendoex  35646
  Copyright terms: Public domain W3C validator