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  3006  rspc2ev  3052  reuss  3614  frc  4540  trssord  4590  funtp  5494  resdif  5687  fnotovb  6108  fovrn  6207  fnovrn  6212  fmpt2co  6421  smoord  6618  odi  6813  oeoa  6831  oeoe  6833  nndi  6857  ecopovtrn  6998  ecovass  7007  ecovdi  7008  supmaxlem  7458  suppr  7462  harval2  7873  cdaassen  8051  fin23lem31  8212  tskuni  8647  addasspi  8761  mulasspi  8763  distrpi  8764  mulcanenq  8826  genpass  8875  distrlem1pr  8891  prlem934  8899  ltapr  8911  le2tri3i  9192  subadd  9297  addsub  9305  subdi  9456  submul2  9463  ltaddsub  9491  leaddsub  9493  divval  9669  div12  9689  diveq1  9697  divneg  9698  divdiv2  9715  ltmulgt11  9859  gt0div  9865  ge0div  9866  uzind3  10352  fnn0ind  10358  qdivcl  10584  irrmul  10588  xrlttr  10722  fzen  11061  modcyc  11264  modcyc2  11265  faclbnd4lem4  11575  lenegsq  12112  moddvds  12847  dvdscmulr  12866  dvdsmulcr  12867  dvds2add  12869  dvds2sub  12870  dvdsleabs  12884  divalg  12911  divalgb  12912  ndvdsadd  12916  gcdcllem3  13001  dvdslegcd  13004  modgcd  13024  absmulgcd  13035  odzval  13165  pcmul  13213  ressid2  13505  ressval2  13506  catcisolem  14249  prf1st  14289  prf2nd  14290  1st2ndprf  14291  curfuncf  14323  curf2ndf  14332  pltval  14405  pospo  14418  joinval  14433  joinval2  14434  meetval  14440  meetval2  14441  lubel  14537  isdlat  14607  spwpr4  14651  laspwcl  14654  lanfwcl  14655  mndcl  14683  issubmnd  14712  prdsmndd  14716  submcl  14741  grpinvid1  14841  grpinvid2  14842  mulgp1  14904  ghmlin  14999  ghmsub  15002  odlem2  15165  gexlem2  15204  lsmvalx  15261  efgtval  15343  cmncom  15416  lssvnegcl  16020  islss3  16023  prdslmodd  16033  evlslem2  16556  zntoslem  16825  unopn  16964  ntrss  17107  innei  17177  t1sep2  17421  metustsymOLD  18579  cncfi  18912  evlseu  19925  quotval  20197  abelthlem2  20336  mudivsum  21212  padicabv  21312  grposn  21791  grpoinvid1  21806  grpoinvid2  21807  grpodivval  21819  gxval  21834  ablo4  21863  ablonncan  21870  issubgoi  21886  ablomul  21931  vcnegsubdi2  22042  nvnpcan  22129  nvmeq0  22133  nvabs  22150  imsdval  22166  ipval  22187  nmorepnf  22257  blo3i  22291  blometi  22292  ipasslem5  22324  hvmulcan  22562  his5  22576  his7  22580  his2sub2  22583  hhssnv  22752  fh1  23108  fh2  23109  cm2j  23110  homcl  23237  homco1  23292  homulass  23293  hoadddi  23294  hosubsub2  23303  braadd  23436  bramul  23437  lnopmul  23458  lnopli  23459  lnopaddmuli  23464  lnopsubmuli  23466  lnfnli  23531  lnfnaddmuli  23536  kbass2  23608  mdexchi  23826  xdivval  24153  unitdivcld  24287  cvmlift2lem7  24984  axsegconlem1  25804  finminlem  26258  ivthALT  26275  exidcl  26488  rngoneglmul  26504  rngonegrmul  26505  divrngcl  26510  crngocom  26548  crngm4  26550  inidl  26577  diophren  26811  monotoddzzfi  26942  rpexpmord  26948  ltrmynn0  26950  ltrmxnn0  26951  lermxnn0  26952  rmyeq  26956  lermy  26957  jm2.21  27002  unxpwdom3  27171  dvconstbi  27466  expgrowth  27467  fnotaovb  27976  frgregordn0  28317  onetansqsecsq  28362  bi3impb  28424  eel132  28657  bnj229  29109  bnj546  29121  bnj570  29130  oposlem  29820  hlsuprexch  30017  ldilcnv  30751  ltrnu  30757  tgrpgrplem  31385  tgrpabl  31387  erngdvlem3  31626  erngdvlem3-rN  31634  dvalveclem  31662  dvhfvadd  31728  dvhgrp  31744  dvhlveclem  31745  djhval2  32036
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