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

Theorem 3impb 1190
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 603 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1188 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  3adant1l  1218  3adant1r  1219  3impdi  1281  rsp2e  2913  vtocl3gf  3167  rspc2ev  3218  reuss  3776  frc  4834  trssord  4884  funtp  5622  resdif  5818  fnotovb  6311  fovrn  6418  fnovrn  6423  fmpt2co  6856  smoord  7028  odi  7220  oeoa  7238  oeoe  7240  nndi  7264  ecopovtrn  7406  ecovass  7410  ecovdi  7411  supmaxlemOLD  7916  suppr  7921  harval2  8369  cdaassen  8553  fin23lem31  8714  tskuni  9150  addasspi  9262  mulasspi  9264  distrpi  9265  mulcanenq  9327  genpass  9376  distrlem1pr  9392  prlem934  9400  ltapr  9412  le2tri3i  9703  subadd  9814  addsub  9822  subdi  9986  submul2  9993  ltaddsub  10022  leaddsub  10024  divval  10205  div12  10225  diveq1  10234  divneg  10235  divdiv2  10252  ltmulgt11  10398  gt0div  10404  ge0div  10405  uzind3  10952  fnn0ind  10959  qdivcl  11204  irrmul  11208  xrlttr  11349  fzen  11706  modcyc  12013  modcyc2  12014  faclbnd4lem4  12356  cshweqdifid  12779  lenegsq  13235  moddvds  14077  dvdscmulr  14096  dvdsmulcr  14097  dvds2add  14099  dvds2sub  14100  dvdsleabs  14116  divalg  14145  divalgb  14146  ndvdsadd  14150  gcdcllem3  14235  dvdslegcd  14238  modgcd  14258  absmulgcd  14269  odzval  14402  pcmul  14459  ressid2  14771  ressval2  14772  catcisolem  15584  prf1st  15672  prf2nd  15673  1st2ndprf  15674  curfuncf  15706  curf2ndf  15715  pltval  15789  pospo  15802  lubel  15951  isdlat  16022  issubmnd  16147  prdsmndd  16152  submcl  16183  grpinvid1  16297  grpinvid2  16298  mulgp1  16367  ghmlin  16471  ghmsub  16474  odlem2  16762  gexlem2  16801  lsmvalx  16858  efgtval  16940  cmncom  17013  lssvnegcl  17797  islss3  17800  prdslmodd  17810  evlslem2  18375  evlseu  18380  zntoslem  18768  maducoeval2  19309  madutpos  19311  madugsum  19312  madurid  19313  m2cpminvid  19421  pm2mpghm  19484  unopn  19579  ntrss  19723  innei  19793  t1sep2  20037  metustsymOLD  21230  metustsym  21231  cncfi  21564  rrxds  21991  quotval  22854  abelthlem2  22993  mudivsum  23913  padicabv  24013  axsegconlem1  24422  frgregordn0  25272  grposn  25415  grpoinvid1  25430  grpoinvid2  25431  grpodivval  25443  gxval  25458  ablo4  25487  ablonncan  25494  issubgoi  25510  ablomul  25555  vcnegsubdi2  25666  nvnpcan  25753  nvmeq0  25757  nvabs  25774  imsdval  25790  ipval  25811  nmorepnf  25881  blo3i  25915  blometi  25916  ipasslem5  25948  hvmulcan  26187  his5  26201  his7  26205  his2sub2  26208  hhssnv  26378  fh1  26734  fh2  26735  cm2j  26736  homcl  26863  homco1  26918  homulass  26919  hoadddi  26920  hosubsub2  26929  braadd  27062  bramul  27063  lnopmul  27084  lnopli  27085  lnopaddmuli  27090  lnopsubmuli  27092  lnfnli  27157  lnfnaddmuli  27162  kbass2  27234  mdexchi  27452  xdivval  27849  resvid2  28053  resvval2  28054  unitdivcld  28118  cvmlift2lem7  29018  finminlem  30376  ivthALT  30393  exidcl  30578  rngoneglmul  30594  rngonegrmul  30595  divrngcl  30600  crngocom  30638  crngm4  30640  inidl  30667  diophren  30986  monotoddzzfi  31117  rpexpmord  31123  ltrmynn0  31125  ltrmxnn0  31126  lermxnn0  31127  rmyeq  31131  lermy  31132  jm2.21  31175  radcnvrat  31436  dvconstbi  31480  expgrowth  31481  fnotaovb  32522  ccatpfx  32637  submgmcl  32854  onetansqsecsq  33545  bi3impb  33639  eel132  33882  bnj229  34343  bnj546  34355  bnj570  34364  oposlem  35304  hlsuprexch  35502  ldilcnv  36236  ltrnu  36242  tgrpgrplem  36872  tgrpabl  36874  erngdvlem3  37113  erngdvlem3-rN  37121  dvalveclem  37149  dvhfvadd  37215  dvhgrp  37231  dvhlveclem  37232  djhval2  37523
  Copyright terms: Public domain W3C validator