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

Theorem 3impb 1149
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 589 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1147 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3adant1l  1176  3adant1r  1177  3impdi  1239  vtocl3gf  2958  rspc2ev  3004  reuss  3566  frc  4490  trssord  4540  funtp  5444  resdif  5637  fnotovb  6057  fovrn  6156  fnovrn  6161  fmpt2co  6370  smoord  6564  odi  6759  oeoa  6777  oeoe  6779  nndi  6803  ecopovtrn  6944  ecovass  6953  ecovdi  6954  supmaxlem  7403  suppr  7407  harval2  7818  cdaassen  7996  fin23lem31  8157  tskuni  8592  addasspi  8706  mulasspi  8708  distrpi  8709  mulcanenq  8771  genpass  8820  distrlem1pr  8836  prlem934  8844  ltapr  8856  le2tri3i  9136  subadd  9241  addsub  9249  subdi  9400  submul2  9407  ltaddsub  9435  leaddsub  9437  divval  9613  div12  9633  diveq1  9641  divneg  9642  divdiv2  9659  ltmulgt11  9803  gt0div  9809  ge0div  9810  uzind3  10296  fnn0ind  10302  qdivcl  10528  irrmul  10532  xrlttr  10666  fzen  11005  modcyc  11204  modcyc2  11205  faclbnd4lem4  11515  lenegsq  12052  moddvds  12787  dvdscmulr  12806  dvdsmulcr  12807  dvds2add  12809  dvds2sub  12810  dvdsleabs  12824  divalg  12851  divalgb  12852  ndvdsadd  12856  gcdcllem3  12941  dvdslegcd  12944  modgcd  12964  absmulgcd  12975  odzval  13105  pcmul  13153  ressid2  13445  ressval2  13446  catcisolem  14189  prf1st  14229  prf2nd  14230  1st2ndprf  14231  curfuncf  14263  curf2ndf  14272  pltval  14345  pospo  14358  joinval  14373  joinval2  14374  meetval  14380  meetval2  14381  lubel  14477  isdlat  14547  spwpr4  14591  laspwcl  14594  lanfwcl  14595  mndcl  14623  issubmnd  14652  prdsmndd  14656  submcl  14681  grpinvid1  14781  grpinvid2  14782  mulgp1  14844  ghmlin  14939  ghmsub  14942  odlem2  15105  gexlem2  15144  lsmvalx  15201  efgtval  15283  cmncom  15356  lssvnegcl  15960  islss3  15963  prdslmodd  15973  evlslem2  16496  zntoslem  16761  unopn  16900  ntrss  17043  innei  17113  t1sep2  17356  metustsym  18476  cncfi  18796  evlseu  19805  quotval  20077  abelthlem2  20216  mudivsum  21092  padicabv  21192  grposn  21652  grpoinvid1  21667  grpoinvid2  21668  grpodivval  21680  gxval  21695  ablo4  21724  ablonncan  21731  issubgoi  21747  ablomul  21792  vcnegsubdi2  21903  nvnpcan  21990  nvmeq0  21994  nvabs  22011  imsdval  22027  ipval  22048  nmorepnf  22118  blo3i  22152  blometi  22153  ipasslem5  22185  hvmulcan  22423  his5  22437  his7  22441  his2sub2  22444  hhssnv  22613  fh1  22969  fh2  22970  cm2j  22971  homcl  23098  homco1  23153  homulass  23154  hoadddi  23155  hosubsub2  23164  braadd  23297  bramul  23298  lnopmul  23319  lnopli  23320  lnopaddmuli  23325  lnopsubmuli  23327  lnfnli  23392  lnfnaddmuli  23397  kbass2  23469  mdexchi  23687  xdivval  24004  unitdivcld  24104  cvmlift2lem7  24776  axsegconlem1  25571  finminlem  26013  ivthALT  26030  exidcl  26243  rngoneglmul  26259  rngonegrmul  26260  divrngcl  26265  crngocom  26303  crngm4  26305  inidl  26332  diophren  26566  monotoddzzfi  26697  rpexpmord  26703  ltrmynn0  26705  ltrmxnn0  26706  lermxnn0  26707  rmyeq  26711  lermy  26712  jm2.21  26757  unxpwdom3  26926  dvconstbi  27221  expgrowth  27222  fnotaovb  27732  onetansqsecsq  27851  bi3impb  27913  eel132  28145  bnj229  28594  bnj546  28606  bnj570  28615  oposlem  29299  hlsuprexch  29496  ldilcnv  30230  ltrnu  30236  tgrpgrplem  30864  tgrpabl  30866  erngdvlem3  31105  erngdvlem3-rN  31113  dvalveclem  31141  dvhfvadd  31207  dvhgrp  31223  dvhlveclem  31224  djhval2  31515
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator