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  2957  rspc2ev  3003  reuss  3565  frc  4489  trssord  4539  funtp  5443  resdif  5636  fnotovb  6056  fovrn  6155  fnovrn  6160  fmpt2co  6369  smoord  6563  odi  6758  oeoa  6776  oeoe  6778  nndi  6802  ecopovtrn  6943  ecovass  6952  ecovdi  6953  supmaxlem  7402  suppr  7406  harval2  7817  cdaassen  7995  fin23lem31  8156  tskuni  8591  addasspi  8705  mulasspi  8707  distrpi  8708  mulcanenq  8770  genpass  8819  distrlem1pr  8835  prlem934  8843  ltapr  8855  le2tri3i  9135  subadd  9240  addsub  9248  subdi  9399  submul2  9406  ltaddsub  9434  leaddsub  9436  divval  9612  div12  9632  diveq1  9640  divneg  9641  divdiv2  9658  ltmulgt11  9802  gt0div  9808  ge0div  9809  uzind3  10295  fnn0ind  10301  qdivcl  10527  irrmul  10531  xrlttr  10665  fzen  11004  modcyc  11203  modcyc2  11204  faclbnd4lem4  11514  lenegsq  12051  moddvds  12786  dvdscmulr  12805  dvdsmulcr  12806  dvds2add  12808  dvds2sub  12809  dvdsleabs  12823  divalg  12850  divalgb  12851  ndvdsadd  12855  gcdcllem3  12940  dvdslegcd  12943  modgcd  12963  absmulgcd  12974  odzval  13104  pcmul  13152  ressid2  13444  ressval2  13445  catcisolem  14188  prf1st  14228  prf2nd  14229  1st2ndprf  14230  curfuncf  14262  curf2ndf  14271  pltval  14344  pospo  14357  joinval  14372  joinval2  14373  meetval  14379  meetval2  14380  lubel  14476  isdlat  14546  spwpr4  14590  laspwcl  14593  lanfwcl  14594  mndcl  14622  issubmnd  14651  prdsmndd  14655  submcl  14680  grpinvid1  14780  grpinvid2  14781  mulgp1  14843  ghmlin  14938  ghmsub  14941  odlem2  15104  gexlem2  15143  lsmvalx  15200  efgtval  15282  cmncom  15355  lssvnegcl  15959  islss3  15962  prdslmodd  15972  evlslem2  16495  zntoslem  16760  unopn  16899  ntrss  17042  innei  17112  t1sep2  17355  metustsym  18475  cncfi  18795  evlseu  19804  quotval  20076  abelthlem2  20215  mudivsum  21091  padicabv  21191  grposn  21651  grpoinvid1  21666  grpoinvid2  21667  grpodivval  21679  gxval  21694  ablo4  21723  ablonncan  21730  issubgoi  21746  ablomul  21791  vcnegsubdi2  21902  nvnpcan  21989  nvmeq0  21993  nvabs  22010  imsdval  22026  ipval  22047  nmorepnf  22117  blo3i  22151  blometi  22152  ipasslem5  22184  hvmulcan  22422  his5  22436  his7  22440  his2sub2  22443  hhssnv  22612  fh1  22968  fh2  22969  cm2j  22970  homcl  23097  homco1  23152  homulass  23153  hoadddi  23154  hosubsub2  23163  braadd  23296  bramul  23297  lnopmul  23318  lnopli  23319  lnopaddmuli  23324  lnopsubmuli  23326  lnfnli  23391  lnfnaddmuli  23396  kbass2  23468  mdexchi  23686  xdivval  24003  unitdivcld  24103  cvmlift2lem7  24775  axsegconlem1  25570  finminlem  26012  ivthALT  26029  exidcl  26242  rngoneglmul  26258  rngonegrmul  26259  divrngcl  26264  crngocom  26302  crngm4  26304  inidl  26331  diophren  26565  monotoddzzfi  26696  rpexpmord  26702  ltrmynn0  26704  ltrmxnn0  26705  lermxnn0  26706  rmyeq  26710  lermy  26711  jm2.21  26756  unxpwdom3  26925  dvconstbi  27220  expgrowth  27221  fnotaovb  27731  onetansqsecsq  27850  bi3impb  27912  eel132  28144  bnj229  28593  bnj546  28605  bnj570  28614  oposlem  29298  hlsuprexch  29495  ldilcnv  30229  ltrnu  30235  tgrpgrplem  30863  tgrpabl  30865  erngdvlem3  31104  erngdvlem3-rN  31112  dvalveclem  31140  dvhfvadd  31206  dvhgrp  31222  dvhlveclem  31223  djhval2  31514
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