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  2846  rspc2ev  2892  reuss  3449  frc  4359  trssord  4409  funtp  5303  resdif  5494  fnotovb  5894  fovrn  5990  fnovrn  5995  fmpt2co  6202  smoord  6382  odi  6577  oeoa  6595  oeoe  6597  nndi  6621  ecopovtrn  6761  ecovass  6770  ecovdi  6771  supmaxlem  7215  suppr  7219  harval2  7630  cdaassen  7808  fin23lem31  7969  tskuni  8405  addasspi  8519  mulasspi  8521  distrpi  8522  mulcanenq  8584  genpass  8633  distrlem1pr  8649  prlem934  8657  ltapr  8669  le2tri3i  8949  subadd  9054  addsub  9062  subdi  9213  submul2  9220  ltaddsub  9248  leaddsub  9250  divval  9426  div12  9446  diveq1  9454  divneg  9455  divdiv2  9472  ltmulgt11  9616  gt0div  9622  ge0div  9623  uzind3  10105  fnn0ind  10111  qdivcl  10337  irrmul  10341  xrlttr  10474  fzen  10811  modcyc  10999  modcyc2  11000  faclbnd4lem4  11309  lenegsq  11804  moddvds  12538  dvdscmulr  12557  dvdsmulcr  12558  dvds2add  12560  dvds2sub  12561  dvdsleabs  12575  divalg  12602  divalgb  12603  ndvdsadd  12607  gcdcllem3  12692  dvdslegcd  12695  modgcd  12715  absmulgcd  12726  odzval  12856  pcmul  12904  ressid2  13196  ressval2  13197  catcisolem  13938  prf1st  13978  prf2nd  13979  1st2ndprf  13980  curfuncf  14012  curf2ndf  14021  pltval  14094  pospo  14107  joinval  14122  joinval2  14123  meetval  14129  meetval2  14130  lubel  14226  isdlat  14296  spwpr4  14340  laspwcl  14343  lanfwcl  14344  mndcl  14372  issubmnd  14401  prdsmndd  14405  submcl  14430  grpinvid1  14530  grpinvid2  14531  mulgp1  14593  ghmlin  14688  ghmsub  14691  odlem2  14854  gexlem2  14893  lsmvalx  14950  efgtval  15032  cmncom  15105  lssvnegcl  15713  islss3  15716  prdslmodd  15726  evlslem2  16249  zntoslem  16510  unopn  16649  ntrss  16792  innei  16862  t1sep2  17097  cncfi  18398  evlseu  19400  quotval  19672  abelthlem2  19808  mudivsum  20679  padicabv  20779  grposn  20882  grpoinvid1  20897  grpoinvid2  20898  grpodivval  20910  gxval  20925  ablo4  20954  ablonncan  20961  issubgoi  20977  ablomul  21022  vcnegsubdi2  21131  nvnpcan  21218  nvmeq0  21222  nvabs  21239  imsdval  21255  ipval  21276  nmorepnf  21346  blo3i  21380  blometi  21381  ipasslem5  21413  hvmulcan  21651  his5  21665  his7  21669  his2sub2  21672  hhssnv  21841  fh1  22197  fh2  22198  cm2j  22199  homcl  22326  homco1  22381  homulass  22382  hoadddi  22383  hosubsub2  22392  braadd  22525  bramul  22526  lnopmul  22547  lnopli  22548  lnopaddmuli  22553  lnopsubmuli  22555  lnfnli  22620  lnfnaddmuli  22625  kbass2  22697  mdexchi  22915  xdivval  23102  unitdivcld  23285  cvmlift2lem7  23840  axsegconlem1  24545  subaddv  25671  cmp2morp  25958  finminlem  26231  ivthALT  26258  lpss2  26468  exidcl  26566  rngoneglmul  26582  rngonegrmul  26583  divrngcl  26588  crngocom  26626  crngm4  26628  inidl  26655  diophren  26896  monotoddzzfi  27027  rpexpmord  27033  ltrmynn0  27035  ltrmxnn0  27036  lermxnn0  27037  rmyeq  27041  lermy  27042  jm2.21  27087  unxpwdom3  27256  dvconstbi  27551  expgrowth  27552  fnotaovb  28058  onetansqsecsq  28231  eel132  28475  bnj229  28916  bnj546  28928  bnj570  28937  oposlem  29373  hlsuprexch  29570  ldilcnv  30304  ltrnu  30310  tgrpgrplem  30938  tgrpabl  30940  erngdvlem3  31179  erngdvlem3-rN  31187  dvalveclem  31215  dvhfvadd  31281  dvhgrp  31297  dvhlveclem  31298  djhval2  31589
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