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

Theorem 3impa 1146
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impa.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3impa  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 587 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1145 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3impdir  1238  syl3an9b  1250  biimp3a  1281  rspec3  2656  rspc3v  2906  raltpg  3697  rextpg  3698  disjiun  4029  opelopabt  4293  ordelinel  4507  3optocl  4782  fun2ssres  5311  funssfv  5559  foco2  5696  f1elima  5803  ot1stg  6150  ot2ndg  6151  smogt  6400  omord2  6581  omword  6584  omass  6594  oeword  6604  nnmass  6638  omabslem  6660  th3q  6783  ecovass  6786  fpmg  6809  f1imaeng  6937  findcard  7113  cdaun  7814  cfsmolem  7912  ingru  8453  addasspi  8535  mulasspi  8537  ltapi  8543  ltmpi  8544  genpass  8649  axpre-ltadd  8805  adddir  8846  leltne  8927  le2tri3i  8965  addsub12  9080  subdir  9230  ltaddsub  9264  leaddsub  9266  recextlem2  9415  div12  9462  divdiv32  9484  divdiv1  9487  lble  9722  fnn0ind  10127  supminf  10321  xrleltne  10495  xrmaxeq  10524  xrmineq  10525  elicc4  10733  iccsplit  10784  elfz  10804  fzrevral  10882  fldiv2  10981  modabs  11013  modsubdir  11024  expgt0  11151  expge0  11154  expge1  11155  mulexpz  11158  expp1z  11166  expm1  11167  digit2  11250  digit1  11251  faclbnd4  11326  faclbnd5  11327  ccatval1  11447  absdiflt  11817  absdifle  11818  binom  12304  cos01gt0  12487  rpnnen2lem4  12512  dvds0lem  12555  dvdsnegb  12562  muldvds1  12569  muldvds2  12570  dvdscmulr  12573  dvdsmulcr  12574  gcdaddm  12724  prmdvdsexp  12809  rpexp1i  12816  monpropd  13656  prfval  13989  xpcpropd  13998  curf2ndf  14037  lubub  14239  lubl  14240  eqglact  14684  mndodcongi  14874  oddvdsnn0  14875  efgi0  15045  efgi1  15046  lss0cl  15720  ipcl  16553  opnneiss  16871  cnpval  16982  cnf2  16995  llyi  17216  nllyi  17217  ptpjcn  17321  cnmptk2  17396  flfval  17701  cnmpt2plusg  17787  cnmpt2vsca  17893  xbln0  17981  blssec  17997  blpnfctr  17998  mopni2  18055  mopni3  18056  nmoval  18240  nmocl  18245  isnghm2  18249  isnmhm2  18277  cnmpt2ds  18364  metdseq0  18374  cnmpt2ip  18691  caucfil  18725  mbfimasn  19005  dvnf  19292  dvnbss  19293  coemul  19649  dvply1  19680  dvnply2  19683  pserdvlem2  19820  logeftb  19953  advlogexp  20018  cxpne0  20040  cxpp1  20043  logrec  20133  lgsne0  20588  grposn  20898  issubgoi  20993  ablomul  21038  sspval  21315  sspnval  21329  lnof  21349  lnocoi  21351  nmooval  21357  nmooge0  21361  nmoub3i  21367  bloln  21378  nmblore  21380  hvaddsubass  21636  hvmulcan2  21668  hhssnv  21857  hosval  22336  homval  22337  hodval  22338  hfsval  22339  hfmval  22340  homco1  22397  homulass  22398  hoadddir  22400  hoaddsubass  22411  hosubsub4  22414  nmopub2tALT  22505  nmfnleub2  22522  kbval  22550  lnopmul  22563  lnopmulsubi  22572  0lnfn  22581  lnopcoi  22599  nmcoplb  22626  nmcfnlb  22650  kbass2  22713  nmopleid  22735  hstoh  22828  mdi  22891  dmdi  22898  dmdi4  22903  mdsl3  22912  cdj3lem2  23031  supxrnemnf  23271  iccgelb  23281  umgrass  23886  umgran0  23887  umgrale  23888  dedekind  24097  elno2  24379  ax5seglem9  24637  valpr  25261  prjmapcp  25268  cnfilca  25659  plimfil  25661  fnessex  26378  fzmul  26546  incsequz2  26562  nninfnub  26564  exidreslem  26670  ghomf  26675  rngohomf  26700  rngohom1  26702  rngohomadd  26703  rngohommul  26704  rngoiso1o  26713  rngoisohom  26714  igenmin  26792  3anrabdioph  26965  3orrabdioph  26966  rencldnfilem  27006  expmordi  27135  divalgmodcl  27183  jm2.18  27184  jm2.25  27195  jm2.15nn0  27199  addrfv  27777  subrfv  27778  mulvfv  27779  stoweidlem34  27886  stoweidlem48  27900  aovmpt4g  28169  pthdepisspth  28360  bi3impa  28548  bnj563  29088  bnj605  29255  bnj607  29264  bnj1097  29327  lkrcl  29904  lkrf0  29905  omlfh1N  30070  tendoex  31786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator