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

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

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3
21exp31 604 . 2
323imp 1190 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3impdir  1284  syl3an9b  1297  biimp3a  1328  stoic3  1609  rspec3  2830  rspc3v  3222  raltpg  4080  rextpg  4081  disjiun  4442  3optocl  5083  fun2ssres  5634  funssfv  5886  foco2  6051  f1elima  6171  ot1stg  6814  ot2ndg  6815  smogt  7057  omord2  7235  omword  7238  oeword  7258  omabslem  7314  ecovass  7437  fpmg  7464  findcard  7779  cdaun  8573  cfsmolem  8671  ingru  9214  addasspi  9294  mulasspi  9296  ltapi  9302  ltmpi  9303  axpre-ltadd  9565  leltne  9695  dedekind  9765  recextlem2  10205  divdiv32  10277  divdiv1  10280  lble  10520  fnn0ind  10988  supminf  11198  xrleltne  11380  xrmaxeq  11409  xrmineq  11410  iccgelb  11610  elicc4  11620  iccsplit  11682  elfz  11707  fzrevral  11792  modabs  12029  expgt0  12199  expge0  12202  expge1  12203  mulexpz  12206  expp1z  12214  expm1  12215  digit1  12300  faclbnd4  12375  faclbnd5  12376  ccatval1  12595  abssubne0  13149  binom  13642  dvds0lem  13994  dvdsnegb  14001  muldvds1  14008  muldvds2  14009  dvdscmulr  14012  dvdsmulcr  14013  gcdaddm  14167  prmdvdsexp  14255  rpexp1i  14262  monpropd  15132  prfval  15468  xpcpropd  15477  curf2ndf  15516  eqglact  16252  mndodcongi  16567  oddvdsnn0  16568  efgi0  16738  efgi1  16739  lss0cl  17593  scmatscmid  19008  pmatcollpw3fi1lem1  19287  cnpval  19737  cnf2  19750  cnnei  19783  lfinun  20026  ptpjcn  20112  cnmptk2  20187  flfval  20491  cnmpt2plusg  20587  cnmpt2vsca  20697  ustincl  20710  xbln0  20917  blssec  20938  blpnfctr  20939  mopni2  20996  mopni3  20997  nmoval  21222  nmocl  21227  isnghm2  21231  isnmhm2  21259  cnmpt2ds  21348  metdseq0  21358  cnmpt2ip  21688  caucfil  21722  mbfimasn  22041  dvnf  22330  dvnbss  22331  coemul  22649  dvply1  22680  dvnply2  22683  pserdvlem2  22823  logeftb  22968  advlogexp  23036  cxpne0  23058  cxpp1  23061  lgsne0  23608  f1otrg  24174  ax5seglem9  24240  umgrass  24319  umgran0  24320  umgrale  24321  nbgraf1olem3  24443  pthdepisspth  24576  grposn  25217  sspval  25636  sspnval  25650  lnof  25670  nmooval  25678  nmooge0  25682  nmoub3i  25688  bloln  25699  nmblore  25701  hosval  26659  homval  26660  hodval  26661  hfsval  26662  hfmval  26663  homulass  26721  hoadddir  26723  nmopub2tALT  26828  nmfnleub2  26845  kbval  26873  lnopmul  26886  0lnfn  26904  lnopcoi  26922  nmcoplb  26949  nmcfnlb  26973  kbass2  27036  nmopleid  27058  hstoh  27151  mdi  27214  dmdi  27221  dmdi4  27226  supxrnemnf  27583  reofld  27830  elno2  29414  ftc1anclem2  30091  fzmul  30233  nninfnub  30244  exidreslem  30339  ghomf  30344  rngohomf  30369  rngohom1  30371  rngohomadd  30372  rngohommul  30373  rngoiso1o  30382  rngoisohom  30383  igenmin  30461  3anrabdioph  30716  3orrabdioph  30717  rencldnfilem  30754  expmordi  30883  divalgmodcl  30929  jm2.18  30930  jm2.25  30941  jm2.15nn0  30945  lcmdvds  31214  addrfv  31378  subrfv  31379  mulvfv  31380  ssfiunibd  31509  dvnmul  31740  stoweidlem34  31816  stoweidlem48  31830  aovmpt4g  32286  bi3impa  33253  ex3  33344  bnj605  33965  bnj607  33974  bnj1097  34037  lkrcl  34817  lkrf0  34818  omlfh1N  34983  tendoex  36701
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