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

Theorem 3impa 1182
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 1181 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  3impdir  1274  syl3an9b  1287  biimp3a  1318  thema3  1583  rspec3  2814  rspc3v  3080  raltpg  3925  rextpg  3926  disjiun  4280  opelopabt  4599  ordelinel  4815  3optocl  4913  fun2ssres  5457  funssfv  5703  foco2  5861  f1elima  5974  ot1stg  6589  ot2ndg  6590  smogt  6826  omord2  7004  omword  7007  omass  7017  oeword  7027  nnmass  7061  omabslem  7083  th3q  7207  ecovass  7210  fpmg  7236  f1imaeng  7367  findcard  7549  cdaun  8339  cfsmolem  8437  ingru  8980  addasspi  9062  mulasspi  9064  ltapi  9070  ltmpi  9071  genpass  9176  axpre-ltadd  9332  adddir  9375  leltne  9462  le2tri3i  9502  dedekind  9531  addsub12  9621  subdir  9777  ltaddsub  9811  leaddsub  9813  recextlem2  9965  div12  10014  divdiv32  10037  divdiv1  10040  lble  10280  fnn0ind  10739  supminf  10940  xrleltne  11120  xrmaxeq  11149  xrmineq  11150  iccgelb  11350  elicc4  11360  iccsplit  11416  elfz  11441  fzrevral  11542  fldiv2  11698  modabs  11739  modsubdir  11765  expgt0  11895  expge0  11898  expge1  11899  mulexpz  11902  expp1z  11910  expm1  11911  digit2  11995  digit1  11996  faclbnd4  12071  faclbnd5  12072  ccatval1  12274  abssubne0  12802  absdiflt  12803  absdifle  12804  binom  13291  cos01gt0  13473  rpnnen2lem4  13498  dvds0lem  13541  dvdsnegb  13548  muldvds1  13555  muldvds2  13556  dvdscmulr  13559  dvdsmulcr  13560  gcdaddm  13711  prmdvdsexp  13798  rpexp1i  13805  monpropd  14674  prfval  15007  xpcpropd  15016  curf2ndf  15055  lubub  15287  lubl  15288  eqglact  15730  mndodcongi  16044  oddvdsnn0  16045  efgi0  16215  efgi1  16216  lss0cl  17026  ipcl  18060  opnneiss  18720  cnpval  18838  cnf2  18851  cnnei  18884  llyi  19076  nllyi  19077  ptpjcn  19182  cnmptk2  19257  flfval  19561  cnmpt2plusg  19657  cnmpt2vsca  19767  ustincl  19780  xbln0  19987  blssec  20008  blpnfctr  20009  mopni2  20066  mopni3  20067  nmoval  20292  nmocl  20297  isnghm2  20301  isnmhm2  20329  cnmpt2ds  20418  metdseq0  20428  cnmpt2ip  20758  caucfil  20792  mbfimasn  21110  dvnf  21399  dvnbss  21400  coemul  21717  dvply1  21748  dvnply2  21751  pserdvlem2  21891  logeftb  22030  advlogexp  22098  cxpne0  22120  cxpp1  22123  logrec  22213  lgsne0  22670  f1otrg  23115  ax5seglem9  23181  umgrass  23251  umgran0  23252  umgrale  23253  nbgraf1olem3  23350  pthdepisspth  23471  grposn  23700  issubgoi  23795  ablomul  23840  sspval  24119  sspnval  24133  lnof  24153  lnocoi  24155  nmooval  24161  nmooge0  24165  nmoub3i  24171  bloln  24182  nmblore  24184  hvaddsubass  24441  hvmulcan2  24473  hhssnv  24663  hosval  25142  homval  25143  hodval  25144  hfsval  25145  hfmval  25146  homco1  25203  homulass  25204  hoadddir  25206  hoaddsubass  25217  hosubsub4  25220  nmopub2tALT  25311  nmfnleub2  25328  kbval  25356  lnopmul  25369  lnopmulsubi  25378  0lnfn  25387  lnopcoi  25405  nmcoplb  25432  nmcfnlb  25456  kbass2  25519  nmopleid  25541  hstoh  25634  mdi  25697  dmdi  25704  dmdi4  25709  mdsl3  25718  cdj3lem2  25837  ffs2  26026  supxrnemnf  26054  reofld  26306  elno2  27793  ftc1anclem2  28465  fnessex  28544  fzmul  28633  incsequz2  28642  nninfnub  28644  exidreslem  28739  ghomf  28744  rngohomf  28769  rngohom1  28771  rngohomadd  28772  rngohommul  28773  rngoiso1o  28782  rngoisohom  28783  igenmin  28861  3anrabdioph  29118  3orrabdioph  29119  rencldnfilem  29156  expmordi  29285  divalgmodcl  29333  jm2.18  29334  jm2.25  29345  jm2.15nn0  29349  addrfv  29722  subrfv  29723  mulvfv  29724  stoweidlem34  29826  stoweidlem48  29840  aovmpt4g  30104  ccatw2s1cl  30264  bi3impa  31185  bnj563  31732  bnj605  31897  bnj607  31906  bnj1097  31969  lkrcl  32734  lkrf0  32735  omlfh1N  32900  tendoex  34616
  Copyright terms: Public domain W3C validator