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

Theorem 3impb 1192
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 605 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1190 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  3adant1l  1220  3adant1r  1221  3impdi  1283  vtocl3gf  3174  rspc2ev  3225  reuss  3779  frc  4845  trssord  4895  funtp  5640  resdif  5836  fnotovb  6323  fovrn  6429  fnovrn  6434  fmpt2co  6866  smoord  7036  odi  7228  oeoa  7246  oeoe  7248  nndi  7272  ecopovtrn  7414  ecovass  7418  ecovdi  7419  supmaxlem  7924  suppr  7929  harval2  8378  cdaassen  8562  fin23lem31  8723  tskuni  9161  addasspi  9273  mulasspi  9275  distrpi  9276  mulcanenq  9338  genpass  9387  distrlem1pr  9403  prlem934  9411  ltapr  9423  le2tri3i  9714  subadd  9823  addsub  9831  subdi  9990  submul2  9997  ltaddsub  10026  leaddsub  10028  divval  10209  div12  10229  diveq1  10238  divneg  10239  divdiv2  10256  ltmulgt11  10402  gt0div  10408  ge0div  10409  uzind3  10954  fnn0ind  10960  qdivcl  11203  irrmul  11207  xrlttr  11346  fzen  11703  modcyc  11999  modcyc2  12000  faclbnd4lem4  12342  cshweqdifid  12751  lenegsq  13116  moddvds  13854  dvdscmulr  13873  dvdsmulcr  13874  dvds2add  13876  dvds2sub  13877  dvdsleabs  13891  divalg  13920  divalgb  13921  ndvdsadd  13925  gcdcllem3  14010  dvdslegcd  14013  modgcd  14033  absmulgcd  14044  odzval  14177  pcmul  14234  ressid2  14543  ressval2  14544  catcisolem  15291  prf1st  15331  prf2nd  15332  1st2ndprf  15333  curfuncf  15365  curf2ndf  15374  pltval  15447  pospo  15460  lubel  15609  isdlat  15680  mndcl  15737  issubmnd  15767  prdsmndd  15772  submcl  15803  grpinvid1  15908  grpinvid2  15909  mulgp1  15978  ghmlin  16077  ghmsub  16080  odlem2  16369  gexlem2  16408  lsmvalx  16465  efgtval  16547  cmncom  16620  lssvnegcl  17402  islss3  17405  prdslmodd  17415  evlslem2  17979  evlseu  17984  zntoslem  18390  maducoeval2  18937  madutpos  18939  madugsum  18940  madurid  18941  m2cpminvid  19049  pm2mpghm  19112  unopn  19207  ntrss  19350  innei  19420  t1sep2  19664  metustsymOLD  20827  cncfi  21161  rrxds  21588  quotval  22450  abelthlem2  22589  mudivsum  23471  padicabv  23571  axsegconlem1  23924  frgregordn0  24775  grposn  24921  grpoinvid1  24936  grpoinvid2  24937  grpodivval  24949  gxval  24964  ablo4  24993  ablonncan  25000  issubgoi  25016  ablomul  25061  vcnegsubdi2  25172  nvnpcan  25259  nvmeq0  25263  nvabs  25280  imsdval  25296  ipval  25317  nmorepnf  25387  blo3i  25421  blometi  25422  ipasslem5  25454  hvmulcan  25693  his5  25707  his7  25711  his2sub2  25714  hhssnv  25884  fh1  26240  fh2  26241  cm2j  26242  homcl  26369  homco1  26424  homulass  26425  hoadddi  26426  hosubsub2  26435  braadd  26568  bramul  26569  lnopmul  26590  lnopli  26591  lnopaddmuli  26596  lnopsubmuli  26598  lnfnli  26663  lnfnaddmuli  26668  kbass2  26740  mdexchi  26958  xdivval  27311  resvid2  27509  resvval2  27510  unitdivcld  27547  signstfvc  28199  cvmlift2lem7  28422  finminlem  29741  ivthALT  29758  exidcl  29969  rngoneglmul  29985  rngonegrmul  29986  divrngcl  29991  crngocom  30029  crngm4  30031  inidl  30058  diophren  30379  monotoddzzfi  30510  rpexpmord  30516  ltrmynn0  30518  ltrmxnn0  30519  lermxnn0  30520  rmyeq  30524  lermy  30525  jm2.21  30568  dvconstbi  30867  expgrowth  30868  fnotaovb  31778  onetansqsecsq  32254  bi3impb  32349  eel132  32586  bnj229  33039  bnj546  33051  bnj570  33060  oposlem  33997  hlsuprexch  34195  ldilcnv  34929  ltrnu  34935  tgrpgrplem  35563  tgrpabl  35565  erngdvlem3  35804  erngdvlem3-rN  35812  dvalveclem  35840  dvhfvadd  35906  dvhgrp  35922  dvhlveclem  35923  djhval2  36214
  Copyright terms: Public domain W3C validator