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

Theorem 3impb 1184
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 1182 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  3adant1l  1211  3adant1r  1212  3impdi  1274  vtocl3gf  3137  rspc2ev  3186  reuss  3738  frc  4793  trssord  4843  funtp  5577  resdif  5768  fnotovb  6237  fovrn  6342  fnovrn  6347  fmpt2co  6765  smoord  6935  odi  7127  oeoa  7145  oeoe  7147  nndi  7171  ecopovtrn  7312  ecovass  7321  ecovdi  7322  supmaxlem  7824  suppr  7828  harval2  8277  cdaassen  8461  fin23lem31  8622  tskuni  9060  addasspi  9174  mulasspi  9176  distrpi  9177  mulcanenq  9239  genpass  9288  distrlem1pr  9304  prlem934  9312  ltapr  9324  le2tri3i  9614  subadd  9723  addsub  9731  subdi  9888  submul2  9895  ltaddsub  9923  leaddsub  9925  divval  10106  div12  10126  diveq1  10135  divneg  10136  divdiv2  10153  ltmulgt11  10299  gt0div  10305  ge0div  10306  uzind3  10845  fnn0ind  10851  qdivcl  11084  irrmul  11088  xrlttr  11227  fzen  11583  modcyc  11859  modcyc2  11860  faclbnd4lem4  12188  cshweqdifid  12571  lenegsq  12925  moddvds  13659  dvdscmulr  13678  dvdsmulcr  13679  dvds2add  13681  dvds2sub  13682  dvdsleabs  13696  divalg  13724  divalgb  13725  ndvdsadd  13729  gcdcllem3  13814  dvdslegcd  13817  modgcd  13837  absmulgcd  13848  odzval  13980  pcmul  14035  ressid2  14344  ressval2  14345  catcisolem  15092  prf1st  15132  prf2nd  15133  1st2ndprf  15134  curfuncf  15166  curf2ndf  15175  pltval  15248  pospo  15261  lubel  15410  isdlat  15481  mndcl  15538  issubmnd  15567  prdsmndd  15572  submcl  15599  grpinvid1  15704  grpinvid2  15705  mulgp1  15771  ghmlin  15870  ghmsub  15873  odlem2  16162  gexlem2  16201  lsmvalx  16258  efgtval  16340  cmncom  16413  lssvnegcl  17159  islss3  17162  prdslmodd  17172  evlslem2  17720  evlseu  17725  zntoslem  18113  maducoeval2  18577  madutpos  18579  madugsum  18580  madurid  18581  unopn  18647  ntrss  18790  innei  18860  t1sep2  19104  metustsymOLD  20267  cncfi  20601  rrxds  21028  quotval  21890  abelthlem2  22029  mudivsum  22911  padicabv  23011  axsegconlem1  23314  grposn  23853  grpoinvid1  23868  grpoinvid2  23869  grpodivval  23881  gxval  23896  ablo4  23925  ablonncan  23932  issubgoi  23948  ablomul  23993  vcnegsubdi2  24104  nvnpcan  24191  nvmeq0  24195  nvabs  24212  imsdval  24228  ipval  24249  nmorepnf  24319  blo3i  24353  blometi  24354  ipasslem5  24386  hvmulcan  24625  his5  24639  his7  24643  his2sub2  24646  hhssnv  24816  fh1  25172  fh2  25173  cm2j  25174  homcl  25301  homco1  25356  homulass  25357  hoadddi  25358  hosubsub2  25367  braadd  25500  bramul  25501  lnopmul  25522  lnopli  25523  lnopaddmuli  25528  lnopsubmuli  25530  lnfnli  25595  lnfnaddmuli  25600  kbass2  25672  mdexchi  25890  xdivval  26238  resvid2  26440  resvval2  26441  unitdivcld  26475  signstfvc  27118  cvmlift2lem7  27341  finminlem  28660  ivthALT  28677  exidcl  28888  rngoneglmul  28904  rngonegrmul  28905  divrngcl  28910  crngocom  28948  crngm4  28950  inidl  28977  diophren  29299  monotoddzzfi  29430  rpexpmord  29436  ltrmynn0  29438  ltrmxnn0  29439  lermxnn0  29440  rmyeq  29444  lermy  29445  jm2.21  29490  dvconstbi  29755  expgrowth  29756  fnotaovb  30251  frgregordn0  30810  m2pminv  31223  pm2mpghm  31288  onetansqsecsq  31409  bi3impb  31504  eel132  31741  bnj229  32194  bnj546  32206  bnj570  32215  oposlem  33150  hlsuprexch  33348  ldilcnv  34082  ltrnu  34088  tgrpgrplem  34716  tgrpabl  34718  erngdvlem3  34957  erngdvlem3-rN  34965  dvalveclem  34993  dvhfvadd  35059  dvhgrp  35075  dvhlveclem  35076  djhval2  35367
  Copyright terms: Public domain W3C validator