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  2847  rspc2ev  2893  reuss  3450  frc  4358  trssord  4408  funtp  5269  resdif  5460  fnotovb  5856  fovrn  5952  fnovrn  5957  fmpt2co  6164  smoord  6378  odi  6573  oeoa  6591  oeoe  6593  nndi  6617  ecopovtrn  6757  ecovass  6766  ecovdi  6767  supmaxlem  7211  suppr  7215  harval2  7626  cdaassen  7804  fin23lem31  7965  tskuni  8401  addasspi  8515  mulasspi  8517  distrpi  8518  mulcanenq  8580  genpass  8629  distrlem1pr  8645  prlem934  8653  ltapr  8665  le2tri3i  8945  subadd  9050  addsub  9058  subdi  9209  submul2  9216  ltaddsub  9244  leaddsub  9246  divval  9422  div12  9442  diveq1  9450  divneg  9451  divdiv2  9468  ltmulgt11  9612  gt0div  9618  ge0div  9619  uzind3  10101  fnn0ind  10106  qdivcl  10333  irrmul  10337  xrlttr  10470  fzen  10807  modcyc  10995  modcyc2  10996  faclbnd4lem4  11305  lenegsq  11800  moddvds  12534  dvdscmulr  12553  dvdsmulcr  12554  dvds2add  12556  dvds2sub  12557  dvdsleabs  12571  divalg  12598  divalgb  12599  ndvdsadd  12603  gcdcllem3  12688  dvdslegcd  12691  modgcd  12711  absmulgcd  12722  odzval  12852  pcmul  12900  ressid2  13192  ressval2  13193  catcisolem  13934  prf1st  13974  prf2nd  13975  1st2ndprf  13976  curfuncf  14008  curf2ndf  14017  pltval  14090  pospo  14103  joinval  14118  joinval2  14119  meetval  14125  meetval2  14126  lubel  14222  isdlat  14292  spwpr4  14336  laspwcl  14339  lanfwcl  14340  mndcl  14368  issubmnd  14397  prdsmndd  14401  submcl  14426  grpinvid1  14526  grpinvid2  14527  mulgp1  14589  ghmlin  14684  ghmsub  14687  odlem2  14850  gexlem2  14889  lsmvalx  14946  efgtval  15028  cmncom  15101  lssvnegcl  15709  islss3  15712  prdslmodd  15722  evlslem2  16245  zntoslem  16506  unopn  16645  ntrss  16788  innei  16858  t1sep2  17093  cncfi  18394  evlseu  19396  quotval  19668  abelthlem2  19804  mudivsum  20675  padicabv  20775  grposn  20876  grpoinvid1  20891  grpoinvid2  20892  grpodivval  20904  gxval  20919  ablo4  20948  ablonncan  20955  issubgoi  20971  ablomul  21016  vcnegsubdi2  21125  nvnpcan  21212  nvmeq0  21216  nvabs  21233  imsdval  21249  ipval  21270  nmorepnf  21340  blo3i  21374  blometi  21375  ipasslem5  21407  hvmulcan  21647  his5  21661  his7  21665  his2sub2  21668  hhssnv  21837  fh1  22193  fh2  22194  cm2j  22195  homcl  22322  homco1  22377  homulass  22378  hoadddi  22379  hosubsub2  22388  braadd  22521  bramul  22522  lnopmul  22543  lnopli  22544  lnopaddmuli  22549  lnopsubmuli  22551  lnfnli  22616  lnfnaddmuli  22621  kbass2  22693  mdexchi  22911  cvmlift2lem7  23247  axsegconlem1  23955  subaddv  25082  cmp2morp  25369  finminlem  25642  ivthALT  25669  lpss2  25879  exidcl  25977  rngoneglmul  25993  rngonegrmul  25994  divrngcl  25999  crngocom  26037  crngm4  26039  inidl  26066  diophren  26307  monotoddzzfi  26438  rpexpmord  26444  ltrmynn0  26446  ltrmxnn0  26447  lermxnn0  26448  rmyeq  26452  lermy  26453  jm2.21  26498  unxpwdom3  26667  dvconstbi  26962  expgrowth  26963  fnotaovb  27449  onetansqsecsq  27503  eel132  27755  bnj229  28195  bnj546  28207  bnj570  28216  oposlem  28652  hlsuprexch  28849  ldilcnv  29583  ltrnu  29589  tgrpgrplem  30217  tgrpabl  30219  erngdvlem3  30458  erngdvlem3-rN  30466  dvalveclem  30494  dvhfvadd  30560  dvhgrp  30576  dvhlveclem  30577  djhval2  30868
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