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

Theorem 3impa 1146
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 587 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1145 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3impdir  1238  syl3an9b  1250  biimp3a  1281  rspec3  2643  rspc3v  2893  raltpg  3684  rextpg  3685  disjiun  4013  opelopabt  4277  ordelinel  4491  3optocl  4766  fun2ssres  5295  funssfv  5543  foco2  5680  f1elima  5787  ot1stg  6134  ot2ndg  6135  smogt  6384  omord2  6565  omword  6568  omass  6578  oeword  6588  nnmass  6622  omabslem  6644  th3q  6767  ecovass  6770  fpmg  6793  f1imaeng  6921  findcard  7097  cdaun  7798  cfsmolem  7896  ingru  8437  addasspi  8519  mulasspi  8521  ltapi  8527  ltmpi  8528  genpass  8633  axpre-ltadd  8789  adddir  8830  leltne  8911  le2tri3i  8949  addsub12  9064  subdir  9214  ltaddsub  9248  leaddsub  9250  recextlem2  9399  div12  9446  divdiv32  9468  divdiv1  9471  lble  9706  fnn0ind  10111  supminf  10305  xrleltne  10479  xrmaxeq  10508  xrmineq  10509  elicc4  10717  iccsplit  10768  elfz  10788  fzrevral  10866  fldiv2  10965  modabs  10997  modsubdir  11008  expgt0  11135  expge0  11138  expge1  11139  mulexpz  11142  expp1z  11150  expm1  11151  digit2  11234  digit1  11235  faclbnd4  11310  faclbnd5  11311  ccatval1  11431  absdiflt  11801  absdifle  11802  binom  12288  cos01gt0  12471  rpnnen2lem4  12496  dvds0lem  12539  dvdsnegb  12546  muldvds1  12553  muldvds2  12554  dvdscmulr  12557  dvdsmulcr  12558  gcdaddm  12708  prmdvdsexp  12793  rpexp1i  12800  monpropd  13640  prfval  13973  xpcpropd  13982  curf2ndf  14021  lubub  14223  lubl  14224  eqglact  14668  mndodcongi  14858  oddvdsnn0  14859  efgi0  15029  efgi1  15030  lss0cl  15704  ipcl  16537  opnneiss  16855  cnpval  16966  cnf2  16979  llyi  17200  nllyi  17201  ptpjcn  17305  cnmptk2  17380  flfval  17685  cnmpt2plusg  17771  cnmpt2vsca  17877  xbln0  17965  blssec  17981  blpnfctr  17982  mopni2  18039  mopni3  18040  nmoval  18224  nmocl  18229  isnghm2  18233  isnmhm2  18261  cnmpt2ds  18348  metdseq0  18358  cnmpt2ip  18675  caucfil  18709  mbfimasn  18989  dvnf  19276  dvnbss  19277  coemul  19633  dvply1  19664  dvnply2  19667  pserdvlem2  19804  logeftb  19937  advlogexp  20002  cxpne0  20024  cxpp1  20027  logrec  20117  lgsne0  20572  grposn  20882  issubgoi  20977  ablomul  21022  sspval  21299  sspnval  21313  lnof  21333  lnocoi  21335  nmooval  21341  nmooge0  21345  nmoub3i  21351  bloln  21362  nmblore  21364  hvaddsubass  21620  hvmulcan2  21652  hhssnv  21841  hosval  22320  homval  22321  hodval  22322  hfsval  22323  hfmval  22324  homco1  22381  homulass  22382  hoadddir  22384  hoaddsubass  22395  hosubsub4  22398  nmopub2tALT  22489  nmfnleub2  22506  kbval  22534  lnopmul  22547  lnopmulsubi  22556  0lnfn  22565  lnopcoi  22583  nmcoplb  22610  nmcfnlb  22634  kbass2  22697  nmopleid  22719  hstoh  22812  mdi  22875  dmdi  22882  dmdi4  22887  mdsl3  22896  cdj3lem2  23015  umgrass  23282  umgran0  23283  umgrale  23284  dedekind  23493  elno2  23719  ax5seglem9  23976  valpr  24570  prjmapcp  24577  cnfilca  24968  plimfil  24970  fnessex  25687  fzmul  25855  incsequz2  25871  nninfnub  25873  exidreslem  25979  ghomf  25984  rngohomf  26009  rngohom1  26011  rngohomadd  26012  rngohommul  26013  rngoiso1o  26022  rngoisohom  26023  igenmin  26101  3anrabdioph  26274  3orrabdioph  26275  rencldnfilem  26315  expmordi  26444  divalgmodcl  26492  jm2.18  26493  jm2.25  26504  jm2.15nn0  26508  addrfv  27086  subrfv  27087  mulvfv  27088  stoweidlem34  27195  stoweidlem48  27209  aovmpt4g  27473  bnj563  28145  bnj605  28312  bnj607  28321  bnj1097  28384  lkrcl  28655  lkrf0  28656  omlfh1N  28821  tendoex  30537
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