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

Theorem 3impa 1149
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 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1148 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3impdir  1241  syl3an9b  1253  biimp3a  1284  rspec3  2808  rspc3v  3063  raltpg  3861  rextpg  3862  disjiun  4204  opelopabt  4469  ordelinel  4682  3optocl  4956  fun2ssres  5496  funssfv  5748  foco2  5891  f1elima  6011  ot1stg  6363  ot2ndg  6364  smogt  6631  omord2  6812  omword  6815  omass  6825  oeword  6835  nnmass  6869  omabslem  6891  th3q  7015  ecovass  7018  fpmg  7041  f1imaeng  7169  findcard  7349  cdaun  8054  cfsmolem  8152  ingru  8692  addasspi  8774  mulasspi  8776  ltapi  8782  ltmpi  8783  genpass  8888  axpre-ltadd  9044  adddir  9085  leltne  9166  le2tri3i  9205  addsub12  9320  subdir  9470  ltaddsub  9504  leaddsub  9506  recextlem2  9655  div12  9702  divdiv32  9724  divdiv1  9727  lble  9962  fnn0ind  10371  supminf  10565  xrleltne  10740  xrmaxeq  10769  xrmineq  10770  elicc4  10979  iccsplit  11031  elfz  11051  fzrevral  11133  fldiv2  11244  modabs  11276  modsubdir  11287  expgt0  11415  expge0  11418  expge1  11419  mulexpz  11422  expp1z  11430  expm1  11431  digit2  11514  digit1  11515  faclbnd4  11590  faclbnd5  11591  ccatval1  11747  abssubne0  12122  absdiflt  12123  absdifle  12124  binom  12611  cos01gt0  12794  rpnnen2lem4  12819  dvds0lem  12862  dvdsnegb  12869  muldvds1  12876  muldvds2  12877  dvdscmulr  12880  dvdsmulcr  12881  gcdaddm  13031  prmdvdsexp  13116  rpexp1i  13123  monpropd  13965  prfval  14298  xpcpropd  14307  curf2ndf  14346  lubub  14548  lubl  14549  eqglact  14993  mndodcongi  15183  oddvdsnn0  15184  efgi0  15354  efgi1  15355  lss0cl  16025  ipcl  16866  opnneiss  17184  cnpval  17302  cnf2  17315  cnnei  17348  llyi  17539  nllyi  17540  ptpjcn  17645  cnmptk2  17720  flfval  18024  cnmpt2plusg  18120  cnmpt2vsca  18226  ustincl  18239  xbln0  18446  blssec  18467  blpnfctr  18468  mopni2  18525  mopni3  18526  nmoval  18751  nmocl  18756  isnghm2  18760  isnmhm2  18788  cnmpt2ds  18876  metdseq0  18886  cnmpt2ip  19204  caucfil  19238  mbfimasn  19528  dvnf  19815  dvnbss  19816  coemul  20172  dvply1  20203  dvnply2  20206  pserdvlem2  20346  logeftb  20480  advlogexp  20548  cxpne0  20570  cxpp1  20573  logrec  20663  lgsne0  21119  umgrass  21356  umgran0  21357  umgrale  21358  nbgraf1olem3  21455  pthdepisspth  21576  grposn  21805  issubgoi  21900  ablomul  21945  sspval  22224  sspnval  22238  lnof  22258  lnocoi  22260  nmooval  22266  nmooge0  22270  nmoub3i  22276  bloln  22287  nmblore  22289  hvaddsubass  22545  hvmulcan2  22577  hhssnv  22766  hosval  23245  homval  23246  hodval  23247  hfsval  23248  hfmval  23249  homco1  23306  homulass  23307  hoadddir  23309  hoaddsubass  23320  hosubsub4  23323  nmopub2tALT  23414  nmfnleub2  23431  kbval  23459  lnopmul  23472  lnopmulsubi  23481  0lnfn  23490  lnopcoi  23508  nmcoplb  23535  nmcfnlb  23559  kbass2  23622  nmopleid  23644  hstoh  23737  mdi  23800  dmdi  23807  dmdi4  23812  mdsl3  23821  cdj3lem2  23940  supxrnemnf  24129  iccgelb  24138  dedekind  25189  elno2  25611  ax5seglem9  25878  ftc1anclem2  26283  fnessex  26357  fzmul  26446  incsequz2  26455  nninfnub  26457  exidreslem  26554  ghomf  26559  rngohomf  26584  rngohom1  26586  rngohomadd  26587  rngohommul  26588  rngoiso1o  26597  rngoisohom  26598  igenmin  26676  3anrabdioph  26843  3orrabdioph  26844  rencldnfilem  26883  expmordi  27012  divalgmodcl  27060  jm2.18  27061  jm2.25  27072  jm2.15nn0  27076  addrfv  27652  subrfv  27653  mulvfv  27654  stoweidlem34  27761  stoweidlem48  27775  aovmpt4g  28043  bi3impa  28629  bnj563  29173  bnj605  29340  bnj607  29349  bnj1097  29412  lkrcl  29952  lkrf0  29953  omlfh1N  30118  tendoex  31834
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