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

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

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 588 . 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:  3adant1l  1174  3adant1r  1175  3impdi  1237  vtocl3gf  2848  rspc2ev  2894  reuss  3451  frc  4361  trssord  4411  funtp  5305  resdif  5496  fnotovb  5896  fovrn  5992  fnovrn  5997  fmpt2co  6204  smoord  6384  odi  6579  oeoa  6597  oeoe  6599  nndi  6623  ecopovtrn  6763  ecovass  6772  ecovdi  6773  supmaxlem  7217  suppr  7221  harval2  7632  cdaassen  7810  fin23lem31  7971  tskuni  8407  addasspi  8521  mulasspi  8523  distrpi  8524  mulcanenq  8586  genpass  8635  distrlem1pr  8651  prlem934  8659  ltapr  8671  le2tri3i  8951  subadd  9056  addsub  9064  subdi  9215  submul2  9222  ltaddsub  9250  leaddsub  9252  divval  9428  div12  9448  diveq1  9456  divneg  9457  divdiv2  9474  ltmulgt11  9618  gt0div  9624  ge0div  9625  uzind3  10107  fnn0ind  10113  qdivcl  10339  irrmul  10343  xrlttr  10476  fzen  10813  modcyc  11001  modcyc2  11002  faclbnd4lem4  11311  lenegsq  11806  moddvds  12540  dvdscmulr  12559  dvdsmulcr  12560  dvds2add  12562  dvds2sub  12563  dvdsleabs  12577  divalg  12604  divalgb  12605  ndvdsadd  12609  gcdcllem3  12694  dvdslegcd  12697  modgcd  12717  absmulgcd  12728  odzval  12858  pcmul  12906  ressid2  13198  ressval2  13199  catcisolem  13940  prf1st  13980  prf2nd  13981  1st2ndprf  13982  curfuncf  14014  curf2ndf  14023  pltval  14096  pospo  14109  joinval  14124  joinval2  14125  meetval  14131  meetval2  14132  lubel  14228  isdlat  14298  spwpr4  14342  laspwcl  14345  lanfwcl  14346  mndcl  14374  issubmnd  14403  prdsmndd  14407  submcl  14432  grpinvid1  14532  grpinvid2  14533  mulgp1  14595  ghmlin  14690  ghmsub  14693  odlem2  14856  gexlem2  14895  lsmvalx  14952  efgtval  15034  cmncom  15107  lssvnegcl  15715  islss3  15718  prdslmodd  15728  evlslem2  16251  zntoslem  16512  unopn  16651  ntrss  16794  innei  16864  t1sep2  17099  cncfi  18400  evlseu  19402  quotval  19674  abelthlem2  19810  mudivsum  20681  padicabv  20781  grposn  20884  grpoinvid1  20899  grpoinvid2  20900  grpodivval  20912  gxval  20927  ablo4  20956  ablonncan  20963  issubgoi  20979  ablomul  21024  vcnegsubdi2  21133  nvnpcan  21220  nvmeq0  21224  nvabs  21241  imsdval  21257  ipval  21278  nmorepnf  21348  blo3i  21382  blometi  21383  ipasslem5  21415  hvmulcan  21653  his5  21667  his7  21671  his2sub2  21674  hhssnv  21843  fh1  22199  fh2  22200  cm2j  22201  homcl  22328  homco1  22383  homulass  22384  hoadddi  22385  hosubsub2  22394  braadd  22527  bramul  22528  lnopmul  22549  lnopli  22550  lnopaddmuli  22555  lnopsubmuli  22557  lnfnli  22622  lnfnaddmuli  22627  kbass2  22699  mdexchi  22917  xdivval  23104  unitdivcld  23287  cvmlift2lem7  23842  axsegconlem1  24547  subaddv  25682  cmp2morp  25969  finminlem  26242  ivthALT  26269  lpss2  26479  exidcl  26577  rngoneglmul  26593  rngonegrmul  26594  divrngcl  26599  crngocom  26637  crngm4  26639  inidl  26666  diophren  26907  monotoddzzfi  27038  rpexpmord  27044  ltrmynn0  27046  ltrmxnn0  27047  lermxnn0  27048  rmyeq  27052  lermy  27053  jm2.21  27098  unxpwdom3  27267  dvconstbi  27562  expgrowth  27563  fnotaovb  28069  onetansqsecsq  28242  bi3impb  28304  eel132  28537  bnj229  28989  bnj546  29001  bnj570  29010  oposlem  29446  hlsuprexch  29643  ldilcnv  30377  ltrnu  30383  tgrpgrplem  31011  tgrpabl  31013  erngdvlem3  31252  erngdvlem3-rN  31260  dvalveclem  31288  dvhfvadd  31354  dvhgrp  31370  dvhlveclem  31371  djhval2  31662
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