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

Theorem 3impb 1192
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1
Assertion
Ref Expression
3impb

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3
21exp32 605 . 2
323imp 1190 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3adant1l  1220  3adant1r  1221  3impdi  1283  rsp2e  2916  vtocl3gf  3170  rspc2ev  3221  reuss  3778  frc  4850  trssord  4900  funtp  5645  resdif  5841  fnotovb  6338  fovrn  6445  fnovrn  6450  fmpt2co  6883  smoord  7055  odi  7247  oeoa  7265  oeoe  7267  nndi  7291  ecopovtrn  7433  ecovass  7437  ecovdi  7438  supmaxlemOLD  7945  suppr  7950  harval2  8399  cdaassen  8583  fin23lem31  8744  tskuni  9182  addasspi  9294  mulasspi  9296  distrpi  9297  mulcanenq  9359  genpass  9408  distrlem1pr  9424  prlem934  9432  ltapr  9444  le2tri3i  9735  subadd  9846  addsub  9854  subdi  10015  submul2  10022  ltaddsub  10051  leaddsub  10053  divval  10234  div12  10254  diveq1  10263  divneg  10264  divdiv2  10281  ltmulgt11  10427  gt0div  10433  ge0div  10434  uzind3  10981  fnn0ind  10988  qdivcl  11232  irrmul  11236  xrlttr  11375  fzen  11732  modcyc  12031  modcyc2  12032  faclbnd4lem4  12374  cshweqdifid  12788  lenegsq  13153  moddvds  13993  dvdscmulr  14012  dvdsmulcr  14013  dvds2add  14015  dvds2sub  14016  dvdsleabs  14032  divalg  14061  divalgb  14062  ndvdsadd  14066  gcdcllem3  14151  dvdslegcd  14154  modgcd  14174  absmulgcd  14185  odzval  14318  pcmul  14375  ressid2  14685  ressval2  14686  catcisolem  15433  prf1st  15473  prf2nd  15474  1st2ndprf  15475  curfuncf  15507  curf2ndf  15516  pltval  15590  pospo  15603  lubel  15752  isdlat  15823  issubmnd  15948  prdsmndd  15953  submcl  15984  grpinvid1  16098  grpinvid2  16099  mulgp1  16168  ghmlin  16272  ghmsub  16275  odlem2  16563  gexlem2  16602  lsmvalx  16659  efgtval  16741  cmncom  16814  lssvnegcl  17602  islss3  17605  prdslmodd  17615  evlslem2  18180  evlseu  18185  zntoslem  18595  maducoeval2  19142  madutpos  19144  madugsum  19145  madurid  19146  m2cpminvid  19254  pm2mpghm  19317  unopn  19412  ntrss  19556  innei  19626  t1sep2  19870  metustsymOLD  21064  metustsym  21065  cncfi  21398  rrxds  21825  quotval  22688  abelthlem2  22827  mudivsum  23715  padicabv  23815  axsegconlem1  24220  frgregordn0  25070  grposn  25217  grpoinvid1  25232  grpoinvid2  25233  grpodivval  25245  gxval  25260  ablo4  25289  ablonncan  25296  issubgoi  25312  ablomul  25357  vcnegsubdi2  25468  nvnpcan  25555  nvmeq0  25559  nvabs  25576  imsdval  25592  ipval  25613  nmorepnf  25683  blo3i  25717  blometi  25718  ipasslem5  25750  hvmulcan  25989  his5  26003  his7  26007  his2sub2  26010  hhssnv  26180  fh1  26536  fh2  26537  cm2j  26538  homcl  26665  homco1  26720  homulass  26721  hoadddi  26722  hosubsub2  26731  braadd  26864  bramul  26865  lnopmul  26886  lnopli  26887  lnopaddmuli  26892  lnopsubmuli  26894  lnfnli  26959  lnfnaddmuli  26964  kbass2  27036  mdexchi  27254  xdivval  27615  resvid2  27818  resvval2  27819  unitdivcld  27883  cvmlift2lem7  28754  finminlem  30136  ivthALT  30153  exidcl  30338  rngoneglmul  30354  rngonegrmul  30355  divrngcl  30360  crngocom  30398  crngm4  30400  inidl  30427  diophren  30747  monotoddzzfi  30878  rpexpmord  30884  ltrmynn0  30886  ltrmxnn0  30887  lermxnn0  30888  rmyeq  30892  lermy  30893  jm2.21  30936  radcnvrat  31195  dvconstbi  31239  expgrowth  31240  fnotaovb  32283  submgmcl  32482  onetansqsecsq  33155  bi3impb  33252  eel132  33488  bnj229  33942  bnj546  33954  bnj570  33963  oposlem  34907  hlsuprexch  35105  ldilcnv  35839  ltrnu  35845  tgrpgrplem  36475  tgrpabl  36477  erngdvlem3  36716  erngdvlem3-rN  36724  dvalveclem  36752  dvhfvadd  36818  dvhgrp  36834  dvhlveclem  36835  djhval2  37126
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
  Copyright terms: Public domain W3C validator